def bit

bend-kit-lemmas@0.1.1.0 · lemmas.bend:13

import Base

13# The value of a word whose low bit is x and whose upper bits have value t.
14def bit(x: Bool, t: Nat) -> Nat:
15  match x:
16    case False{}:
17      Nat.double(t)
18    case True{}:
19      1n+Nat.double(t)