~/bend-docscommunity

proofs/binary_digit.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/binary_digit.bend as Binary_digit

The same binary-digit interpretation serves long division and division by two.

2 imports
import Base
import ./u32_comparison.bend as Comparison

Definitions

def word_digit source · line 5 · raw

@+n:Nat -> @+bit:Bool -> @+w:Word(n) -> {Word.to_nat(1n+n, WCon{bit, w}) == 0x9be3b13bf249759bc81e1958bcd1a4c0/proofs/u32_comparison.digit(bit, Word.to_nat(n, w)) : Nat}