def u32_lt

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

import Base

138def u32_lt(+a: U32, +b: U32) -> {Nat.is_lt(U32.to_nat(a), U32.to_nat(b)) == U32.is_lt(a, b) : Bool}:
139  match a b:
140    case U32{x} U32{y}:
141      %word_cmp(32n, x, y) : {Cmp.is_lt(Nat.cmp(Word.to_nat(32n, x), Word.to_nat(32n, y))) == Cmp.is_lt(_) : Bool}
142      {==}