def zero_nat

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32laws.bend:79

import Base

79# U32.is_zero is the zero test on the value
80def zero_nat(+a: U32) -> {U32.is_zero(a) == Nat.is_eq(v(a), 0n) : Bool}:
81  is_zero_c(a, U32.is_zero(a), {==}, v(a), {==})