def cursor_exact

bendtorch-core@0.1.0.0 · src/tensor/from_values_contract.bend:59

import Base
import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion

59def cursor_exact(+cursor: Nat, +remaining: Nat, +limit: U32,
60  room: {Nat.is_le(Nat.add(cursor, 1n+remaining), U32.to_nat(limit)) == True{} : Bool}) ->
61  {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat}:
62  Conversion.natural_word_exact(cursor, limit, cursor_le(cursor, remaining, U32.to_nat(limit), room))