def room_next

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

import Base
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith

41def room_next(+cursor: Nat, +remaining: Nat, +bound: Nat,
42  room: {Nat.is_le(Nat.add(cursor, 1n+remaining), bound) == True{} : Bool}) ->
43  {Nat.is_le(Nat.add(1n+cursor, remaining), bound) == True{} : Bool}:
44  %Arith.add_succ(cursor, remaining) : {Nat.is_le(_, bound) == True{} : Bool}
45  room