MatmulPROOF.checked_different: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend as MatmulPROOF
Lines 301-307 of bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend&start_line=301&end_line=307

import Base

def checked_different(+position: Nat, +cursor: Nat,
  position_exact: {U32.to_nat(U32.from_nat(position)) == position : Nat}, cursor_exact: {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat},
  earlier: {Nat.is_lt(position, cursor) == True{} : Bool}) ->
  {Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), U32.to_nat(U32.from_nat(position))) == False{} : Bool}:
  %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}
  %Equal.sym(Nat, U32.to_nat(U32.from_nat(position)), position, position_exact) : {Nat.is_eq(cursor, _) == False{} : Bool}
  earlier_different(position, cursor, earlier)

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/matmul_PROOF.bend&name=earlier_different