round an exact signed rational sign x N/M to the format; N = 0 is the signed zero
113def modelRoundBits =
114 (lambda unrestricted sign : Nat . (lambda unrestricted numerator : Nat . (lambda unrestricted denominator : Nat .
115 (specSelect (specIsZero numerator)
116 (modelZeroOf sign)
117 (eliminate SpecResult (lambda unrestricted current : (family SpecResult) . Nat)
118 (specAssemble 8 23 127 sign (specRound 23 127 numerator denominator))
119 (branch SpecBits n . n)
120 (branch SpecOverflow . (modelInfinityOf sign)))))))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.