104def magnitudeRadixScale =
105 (lambda unrestricted radix : (family IntegerLiteralRadix) .
106 (lambda unrestricted digits : Bytes .
107 (eliminate
108 IntegerLiteralRadix
109 (lambda unrestricted current : (family IntegerLiteralRadix) . Bytes)
110 radix
111 (branch IntegerLiteralDecimal . (magnitudeMultiplyDigit digits (byte 10)))
112 (branch IntegerLiteralBinary . (magnitudeDouble digits))
113 (branch
114 IntegerLiteralHexadecimal
115 .
116 (magnitudeRepeatSmall
117 Bytes
118 (byte-to-nat (byte 4))
119 (lambda unrestricted value : Bytes . (magnitudeDouble value))
120 digits)))))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.