def Isqrt.value

bend-collections-laws-crypto@1.0.0.0 · spec/math/w64.bend:99

import Base
import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as W
import bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend as M

99# the integer square root of the proved Nat reference
100def Isqrt.value(+n: W.U64) -> Type:
101  {value(X.isqrt(n)) == M.isqrt(value(n)) : Nat}