def m16

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64sqrt.bend:57

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD

57# 1 + v(m) == 2^16 for m the 16-bit mask
58def m16(+one: Nat, +h1: {one == 1n : Nat}, +m: U32, +pm: {m == U32{WD.mask(32n, 16n)} : U32}) -> {1n+v(m) == WD.sc(16n, one) : Nat}:
59  mask_v(16n, {==}, one, h1, m, pm)