AlphaGitHub
Source/Reference

Float32Model

reference/numeric/Float32Model.alpha

304 lines61 declarations17.2 KiBSHA-256 421f33839d13
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 171–187

modelF32SquareRoot

Full file
171def modelF32SquareRoot =
172  (lambda unrestricted a : Nat .
173    (specSelect (modelIsNaN a)
174      (modelQuiet a)
175      (specSelect (modelIsZero a)
176        a
177        (specSelect (modelSign a)
178          modelDefaultNaN
179          (specSelect (modelIsInfinite a)
180            modelInfinityBits
181            (app (lambda unrestricted n : Nat .
182              (app (lambda unrestricted q : Nat .
183                (modelRoundBits 0
184                  (specSelect (specEqual (nat-multiply q q) n) (nat-multiply 2 q) (nat-add (nat-multiply 2 q) 1))
185                  (nat-multiply 2 modelPow2Hundred50)))
186              (modelIntegerRoot n)))
187            (nat-multiply (modelScaledMagnitude a) modelPow2Hundred50)))))))

The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.