def native_ge_nat

stelliferous@0.0.2.0 · proofs/u32_division.bend:23

import stelliferous@0.0.2.0/proofs/u32_division.bend as U32Division

import Base
import stelliferous@0.0.2.0/proofs/u32_comparison.bend as Comparison

23def native_ge_nat(+a: U32,+b: U32,h: {U32.is_ge(a,b) == True{} : Bool}) -> {Nat.is_ge(U32.to_nat(a),U32.to_nat(b)) == True{} : Bool}:
24  %Comparison.ge(a,b) : {_ == True{} : Bool}
25  h

Uses (6)

Used by (1)

stelliferous@0.0.2.0/proofs/u32_division:fin