law is_lt_nat

bend-lawful-stdlib@0.1.0.0 · src/u32.bend:107

import Base
import bend-lawful-stdlib@0.1.0.0/src/nat.bend as Nat

107# a result of U32.is_lt is the same result of Nat.is_lt on the numbers
108law is_lt_nat:
109  for +a: U32
110  for +b: U32
111  for -c: Bool
112  for e: {U32.is_lt(a, b) == c : Bool}
113  {Nat.is_lt(U32.to_nat(a), U32.to_nat(b)) == c : Bool}