224def magnitudeParseUnsigned =
225 (lambda unrestricted spelling : Bytes .
226 (app
227 (nat-eliminate
228 (lambda unrestricted flag : Nat .
229 (pi unrestricted force : Nat . (family NaturalMagnitudeResult)))
230 (lambda unrestricted force : Nat .
231 (app
232 (nat-eliminate
233 (lambda unrestricted flag : Nat .
234 (pi unrestricted force : Nat . (family NaturalMagnitudeResult)))
235 (lambda unrestricted force : Nat .
236 (magnitudeParseDigits
237 (constructor IntegerLiteralRadix IntegerLiteralDecimal)
238 spelling))
239 (lambda unrestricted predecessor : Nat .
240 (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalMagnitudeResult)) .
241 (lambda unrestricted force : Nat .
242 (app
243 (nat-eliminate
244 (lambda unrestricted flag : Nat .
245 (pi unrestricted force : Nat . (family NaturalMagnitudeResult)))
246 (lambda unrestricted force : Nat .
247 (app
248 (nat-eliminate
249 (lambda unrestricted flag : Nat .
250 (pi unrestricted force : Nat . (family NaturalMagnitudeResult)))
251 (lambda unrestricted force : Nat .
252 (magnitudeParseDigits
253 (constructor IntegerLiteralRadix IntegerLiteralDecimal)
254 spelling))
255 (lambda unrestricted predecessor : Nat .
256 (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalMagnitudeResult)) .
257 (lambda unrestricted force : Nat .
258 (magnitudeParseDigits
259 (constructor IntegerLiteralRadix IntegerLiteralBinary)
260 (bytes-tail (bytes-tail spelling))))))
261 (Std.Natural/naturalOr
262 (byte-equal (bytes-head (bytes-tail spelling)) (byte 98))
263 (byte-equal (bytes-head (bytes-tail spelling)) (byte 66))))
264 zero))
265 (lambda unrestricted predecessor : Nat .
266 (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalMagnitudeResult)) .
267 (lambda unrestricted force : Nat .
268 (magnitudeParseDigits
269 (constructor IntegerLiteralRadix IntegerLiteralHexadecimal)
270 (bytes-tail (bytes-tail spelling))))))
271 (Std.Natural/naturalOr
272 (byte-equal (bytes-head (bytes-tail spelling)) (byte 120))
273 (byte-equal (bytes-head (bytes-tail spelling)) (byte 88))))
274 zero))))
275 (byte-equal (bytes-head spelling) (byte 48)))
276 zero))
277 (lambda unrestricted predecessor : Nat .
278 (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalMagnitudeResult)) .
279 (lambda unrestricted force : Nat .
280 (constructor
281 NaturalMagnitudeResult
282 NaturalMagnitudeRejected
283 (constructor NaturalMagnitudeFailure NaturalMagnitudeNeedsType)))))
284 (byte-equal (bytes-head spelling) (byte 45)))
285 zero))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.