~/jendhub

def checked_different

bendtorch-core@0.1.0.0 · src/tensor/matmul_PROOF.bend:301

import bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend as MatmulPROOF
import Base

301def checked_different(+position: Nat, +cursor: Nat,
302  position_exact: {U32.to_nat(U32.from_nat(position)) == position : Nat}, cursor_exact: {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat},
303  earlier: {Nat.is_lt(position, cursor) == True{} : Bool}) ->
304  {Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), U32.to_nat(U32.from_nat(position))) == False{} : Bool}:
305  %Equal.sym(Nat, U32.to_nat(U32.from_nat(cursor)), cursor, cursor_exact) : {Nat.is_eq(_, U32.to_nat(U32.from_nat(position))) == False{} : Bool}
306  %Equal.sym(Nat, U32.to_nat(U32.from_nat(position)), position, position_exact) : {Nat.is_eq(cursor, _) == False{} : Bool}
307  earlier_different(position, cursor, earlier)

Uses (8)

Used by (1)