def lt_same

bendtorch-core@0.1.0.0 · src/tensor/matrix_index_proof.bend:76

import bendtorch-core@0.1.0.0/src/tensor/matrix_index_proof.bend as MatrixIndexProof

import Base

76def lt_same(-a: Nat, -b: Nat, -bound: Nat, same: {a == b : Nat}, below: {Nat.is_lt(b, bound) == True{} : Bool}) ->
77  {Nat.is_lt(a, bound) == True{} : Bool}:
78  %Equal.sym(Nat, a, b, same) : {Nat.is_lt(_, bound) == True{} : Bool}
79  below

Uses (4)

Used by (3)