def u32_le

bendtorch-core@0.1.0.0 · src/storage/arith.bend:144

import Base

144def u32_le(+a: U32, +b: U32) -> {Nat.is_le(U32.to_nat(a), U32.to_nat(b)) == U32.is_le(a, b) : Bool}:
145  match a b:
146    case U32{x} U32{y}:
147      %word_cmp(32n, x, y) : {Cmp.is_le(Nat.cmp(Word.to_nat(32n, x), Word.to_nat(32n, y))) == Cmp.is_le(_) : Bool}
148      {==}