def native_bound
stelliferous@0.0.2.0 · proofs/nat_to_u32_bounds.bend:35
import stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend as NatToU32Bounds
import Base
import stelliferous@0.0.2.0/proofs/u32_comparison.bend as Comparison
35def native_bound(+n: Nat,+cap: U32,e: {U32.to_nat(U32.from_nat(n)) == n : Nat},h: {Nat.is_lt(n,
36 U32.to_nat(cap)) == True{} : Bool}) -> {U32.is_lt(U32.from_nat(n),cap) == True{} : Bool}:
37 %Equal.sym(Bool,U32.is_lt(U32.from_nat(n),cap),Nat.is_lt(U32.to_nat(U32.from_nat(n)),U32.to_nat(cap)),Comparison.lt(U32.from_nat(n),
38 cap)) : {_ == True{} : Bool}
39 %Equal.sym(Nat,U32.to_nat(U32.from_nat(n)),n,e) : {Nat.is_lt(_,U32.to_nat(cap)) == True{} : Bool}
40 h