def tests_odd

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

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/math/instances.bend as SI
import bend-collections-laws-crypto@1.0.0.0/spec/math/generic.bend as SG
import bend-collections-laws-crypto@1.0.0.0/src/math/instances.bend as I

207def tests_odd(+a: U32) -> SI.Tests.odd(~U32, ~I.u32_is, ~SG.u32_val, a):
208  %Equal.sym(Bool, U32.is_eq(U32.and(a, 1), 1), Nat.is_eq(v(U32.and(a, 1)), v(1)), eq_nat(U32.and(a, 1), 1)) : {_ == Nat.is_eq(Nat.mod(v(a), 2n), 1n) : Bool}
209  %Equal.sym(Nat, v(U32.and(a, 1)), Nat.mod(v(a), 2n), odd_val(a)) : {Nat.is_eq(_, 1n) == Nat.is_eq(Nat.mod(v(a), 2n), 1n) : Bool}
210  {==}