def b32_v

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64mul.bend:218

import Base
import bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S

218def b32_v(+c: Bool) -> {v(X.b32(c)) == S.bit_value(c) : Nat}:
219  match c:
220    case True{}:
221      {==}
222    case False{}:
223      {==}