def cursor_below

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

import Base

232# A cursor with steps left lies below the end.
233def cursor_below(+cursor: Nat, +rest: Nat, +end: Nat, steps: {Nat.add(cursor, 1n+rest) == end : Nat}) ->
234  {Nat.is_lt(cursor, end) == True{} : Bool}:
235  %steps : {Nat.is_lt(cursor, _) == True{} : Bool}
236  lt_add(cursor, rest)