`significand` shifted right by `shift` bits, rounded to nearest, ties to even.
184def stdFloatRoundedShift =
185 (lambda unrestricted significand : Nat .
186 (lambda unrestricted shift : Nat .
187 (nat-eliminate
188 (lambda unrestricted current : Nat . Nat)
189 significand
190 (lambda unrestricted shiftPredecessor : Nat .
191 (lambda unrestricted shiftInduction : Nat .
192 (app
193 (lambda unrestricted scale : Nat .
194 (app
195 (lambda unrestricted quotient : Nat .
196 (app
197 (lambda unrestricted remainder : Nat .
198 (app
199 (lambda unrestricted half : Nat .
200 (nat-add
201 quotient
202 (nat-eliminate
203 (lambda unrestricted current : Nat . Nat)
204 (nat-multiply (naturalEqual remainder half) (nat-modulo quotient 2))
205 (lambda unrestricted abovePredecessor : Nat .
206 (lambda unrestricted aboveInduction : Nat . 1))
207 (nat-less-than half remainder))))
208 (nat-divide scale 2)))
209 (nat-modulo significand scale)))
210 (nat-divide significand scale)))
211 (naturalPowerOfTwo shift))))
212 shift)))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.