def to_nat_con

bend-collections-laws-crypto@1.0.0.0 · proofs/math/random/bits.bend:69

import Base

69# a word's value, its low bit first
70def to_nat_con(+p: Nat, +x: Bool, +t: Word(p)) -> {Word.to_nat(1n+p, WCon{x, t}) == Nat.add(bv(x), Nat.double(Word.to_nat(p, t))) : Nat}:
71  match x:
72    case True{}:
73      {==}
74    case False{}:
75      {==}