def word_digit

stelliferous@0.0.2.0 · proofs/binary_digit.bend:5

import Base
import stelliferous@0.0.2.0/proofs/u32_comparison.bend as Comparison

5def word_digit(+n: Nat,+bit: Bool,+w: Word(n)) -> {Word.to_nat(1n+n,WCon{bit,w}) == Comparison.digit(bit,Word.to_nat(n,w)) : Nat}:
6  match bit:
7    case False{}:
8      {==}
9    case True{}:
10      {==}