law u32_value_eq

bend-osdev-u32@0.1.0.0 · LAWS.bend:163

import bend-osdev-u32@0.1.0.0/LAWS.bend as LAWS
import Base

163law u32_value_eq:
164  for +a: U32
165  for +b: U32
166  for e: {U32.to_nat(a) == U32.to_nat(b) : Nat}
167  {a == b : U32}

Uses (5)

Used by (2)