def child_limit_full

stelliferous@0.0.2.0 · proofs/storage_address_bounds.bend:33

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

33def child_limit_full(+depth: Nat,limit: {Nat.is_le(1n+depth,31n) == True{} : Bool}) -> {Nat.is_le(depth,31n) == True{} : Bool}:
34  Bounds.strict_le(depth,31n,Bounds.predecessor_strict(depth,31n,limit))