def wv.bitw_value

bend-osdev-word64@0.1.1.0 · proof_value.bend:284

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

284def wv.bitw_value(+p: Nat, b: Bool) -> {Word.to_nat(1n+p, wv.bitw(1n+p, b)) == U.U32Nat.bit(b) : Nat}:
285  match b:
286    case True{}:
287      wn.succ_cong(Nat.double(Word.to_nat(p, Word.zero(p))), 0n, Equal.cong(Nat, Nat, v => Nat.double(v), Word.to_nat(p, Word.zero(p)), 0n, UL.word_zero_value(p)))
288    case False{}:
289      Equal.cong(Nat, Nat, v => Nat.double(v), Word.to_nat(p, Word.zero(p)), 0n, UL.word_zero_value(p))