def lt_bound

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

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

import Base

81def lt_bound(-a: Nat, -bound: Nat, -other: Nat, same: {bound == other : Nat}, below: {Nat.is_lt(a, bound) == True{} : Bool}) ->
82  {Nat.is_lt(a, other) == True{} : Bool}:
83  %same : {Nat.is_lt(a, _) == True{} : Bool}
84  below

Uses (3)

Used by (5)