def internal_to_nat_con

bend-mathlib@0.8.1.0 · u32.bend:78

import Base

78def internal_to_nat_con(-p: Nat, b: Bool, -t: Word(p)) -> {Nat.add(internal_bv(b), Nat.double(Word.to_nat(p, t))) == Word.to_nat(1n+p, WCon{b, t}) : Nat}:
79  match b:
80    case False{}:
81      {==}
82    case True{}:
83      {==}