277def modelF32SquareRoot =
278 (lambda unrestricted a : Nat .
279 (specSelect (modelIsNaN a)
280 (modelQuiet a)
281 (specSelect (modelIsZero a)
282 a
283 (specSelect (modelSign a)
284 modelDefaultNaN
285 (specSelect (modelIsInfinite a)
286 modelInfinityBits
287 (app (lambda unrestricted n : Nat .
288 (app (lambda unrestricted q : Nat .
289 (modelRoundBits 0
290 (specSelect (specEqual (nat-multiply q q) n) (nat-multiply 2 q) (nat-add (nat-multiply 2 q) 1))
291 (nat-multiply 2 modelPow2Hundred50)))
292 (modelIntegerRoot n)))
293 (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.