proofs/binary_digit.bend source

proofs/binary_digit.bend on the hub · documented module

# The same binary-digit interpretation serves long division and division by two.import Baseimport ./u32_comparison.bend as Comparisondef 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}:  match bit:    case False{}:      {==}    case True{}:      {==}