def dig1_eq

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64div.bend:115

import Base
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/shrn.bend as SR

115# the high digit is a shift, U32.shrn(lo, 16), the word U32.div(lo, 2^16)
116def dig1_eq(+lo: U32) -> {X.dig1(lo) == d1g(lo, 65536) : Nat}:
117  Equal.cong(U32, Nat, z => U32.to_nat(z), U32.shrn(lo, 16n), U32.div(lo, 65536), SR.shr16(lo))