Part of `jsonParseHexQuad`, lifted out to keep it inside the §28.3 size and
nesting limits; the parameters are the locals it still needs.
425def jsonParseHexQuadPart1 =
426 (lambda unrestricted input : Bytes .
427 (lambda unrestricted a : Byte .
428 (lambda unrestricted b : Byte .
429 (lambda unrestricted c : Byte .
430 (lambda unrestricted d : Byte .
431 (lambda unrestricted remaining : Bytes .
432 (lambda unrestricted remainingInduction : (family JSONHexQuadResult) .
433 (app
434 (lambda unrestricted na : Nat .
435 (app
436 (lambda unrestricted nb : Nat .
437 (app
438 (lambda unrestricted nc : Nat .
439 (app
440 (lambda unrestricted nd : Nat .
441 (nat-eliminate
442 (lambda unrestricted valid : Nat . (family JSONHexQuadResult))
443 (constructor JSONHexQuadResult JSONHexQuadFailed input)
444 (lambda unrestricted predecessor : Nat .
445 (lambda unrestricted induction : (family JSONHexQuadResult) .
446 (constructor
447 JSONHexQuadResult
448 JSONHexQuadParsed
449 (jsonHexQuadValue na nb nc nd)
450 remaining)))
451 (jsonFlagAnd
452 (nat-less-than na jsonNaturalSixteen)
453 (jsonFlagAnd
454 (nat-less-than nb jsonNaturalSixteen)
455 (jsonFlagAnd
456 (nat-less-than nc jsonNaturalSixteen)
457 (nat-less-than nd jsonNaturalSixteen))))))
458 (jsonHexNibble d)))
459 (jsonHexNibble c)))
460 (jsonHexNibble b)))
461 (jsonHexNibble a)))))))))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.