def address_inside

stelliferous@0.0.2.0 · proofs/traversal_map_readback.bend:44

import Base
import stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend as Bounds

44def address_inside(+position: Nat,+capacity: U32,+capacity_ok: {U32.is_le(capacity,2147483648) == True{} : Bool},
45  +inside: {Nat.is_lt(position,U32.to_nat(capacity)) == True{} : Bool}) -> {U32.is_lt(U32.from_nat(position),capacity) == True{} : Bool}:
46  Bounds.native_bound(position,capacity,Bounds.roundtrip(position,capacity,capacity_ok,Bounds.strict_le(position,U32.to_nat(capacity),inside)),inside)