proofs/binary_digit.bend

stelliferous@0.0.2.0 · 10 lines · 1 definition

1# The same binary-digit interpretation serves long division and division by two.
2import Base
3import stelliferous@0.0.2.0/proofs/u32_comparison.bend as Comparison
4
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      {==}