def bo_bit

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/word.bend:38

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

38def bo_bit(+b: Bool, +one: Nat, +h1: {one == 1n : Nat}) -> {bo(b, one) == S.bit_value(b) : Nat}:
39  match b:
40    case True{}:
41      h1
42    case False{}:
43      {==}