def cursor_below

bendtorch-core@0.1.0.0 · src/tensor/contracts/pointwise_proof.bend:73

import bendtorch-core@0.1.0.0/src/tensor/contracts/pointwise_proof.bend as PointwiseProof

import Base

73def cursor_below(+cursor: Nat, +rest: Nat, +end: Nat, steps: {Nat.add(cursor, 1n+rest) == end : Nat}) ->
74  {Nat.is_lt(cursor, end) == True{} : Bool}:
75  %steps : {Nat.is_lt(cursor, _) == True{} : Bool}
76  lt_add(cursor, rest)

Uses (5)

Used by (3)