Data.JSONAccess

595def jsonNumber =
596  (lambda unrestricted value : (family JSON) .
597    (eliminate
598      JSON
599      (lambda unrestricted current : (family JSON) . (family JSONBytesAccessResult))
600      value
601      (branch
602        JSONObject
603        members
604        membersInduction
605        .
606        (constructor
607          JSONBytesAccessResult
608          JSONBytesAccessFailed
609          (constructor JSONErrorCode JSONExpectedNumber)))
610      (branch
611        JSONObjectEnd
612        .
613        (constructor
614          JSONBytesAccessResult
615          JSONBytesAccessFailed
616          (constructor JSONErrorCode JSONExpectedNumber)))
617      (branch
618        JSONObjectMember
619        key
620        member
621        tail
622        memberInduction
623        tailInduction
624        .
625        (constructor
626          JSONBytesAccessResult
627          JSONBytesAccessFailed
628          (constructor JSONErrorCode JSONExpectedNumber)))
629      (branch
630        JSONArray
631        values
632        valuesInduction
633        .
634        (constructor
635          JSONBytesAccessResult
636          JSONBytesAccessFailed
637          (constructor JSONErrorCode JSONExpectedNumber)))
638      (branch
639        JSONArrayEnd
640        .
641        (constructor
642          JSONBytesAccessResult
643          JSONBytesAccessFailed
644          (constructor JSONErrorCode JSONExpectedNumber)))
645      (branch
646        JSONArrayNext
647        head
648        tail
649        headInduction
650        tailInduction
651        .
652        (constructor
653          JSONBytesAccessResult
654          JSONBytesAccessFailed
655          (constructor JSONErrorCode JSONExpectedNumber)))
656      (branch
657        JSONString
658        text
659        .
660        (constructor
661          JSONBytesAccessResult
662          JSONBytesAccessFailed
663          (constructor JSONErrorCode JSONExpectedNumber)))
664      (branch
665        JSONNumber
666        number
667        .
668        (nat-eliminate
669          (lambda unrestricted bounded : Nat . (family JSONBytesAccessResult))
670          (constructor
671            JSONBytesAccessResult
672            JSONBytesAccessFailed
673            (constructor JSONErrorCode JSONNumberLimitExceeded))
674          (lambda unrestricted predecessor : Nat .
675            (lambda unrestricted induction : (family JSONBytesAccessResult) .
676              (eliminate
677                JSONNumberParseResult
678                (lambda unrestricted current : (family JSONNumberParseResult) .
679                  (family JSONBytesAccessResult))
680                (jsonParseNumber number)
681                (branch
682                  JSONNumberParsed
683                  parsed
684                  remaining
685                  .
686                  (nat-eliminate
687                    (lambda unrestricted complete : Nat . (family JSONBytesAccessResult))
688                    (constructor
689                      JSONBytesAccessResult
690                      JSONBytesAccessFailed
691                      (constructor JSONErrorCode JSONExpectedNumber))
692                    (lambda unrestricted completePredecessor : Nat .
693                      (lambda unrestricted completeInduction : (family JSONBytesAccessResult) .
694                        (constructor JSONBytesAccessResult JSONBytesAccessSucceeded parsed)))
695                    (naturalIsZero (bytes-length remaining))))
696                (branch
697                  JSONNumberParseFailed
698                  code
699                  remaining
700                  .
701                  (constructor JSONBytesAccessResult JSONBytesAccessFailed code)))))
702          (jsonNaturalLessThanOrEqual (bytes-length number) jsonNaturalOneThousandTwentyFour)))
703      (branch
704        JSONBoolean
705        boolean
706        .
707        (constructor
708          JSONBytesAccessResult
709          JSONBytesAccessFailed
710          (constructor JSONErrorCode JSONExpectedNumber)))
711      (branch
712        JSONNull
713        .
714        (constructor
715          JSONBytesAccessResult
716          JSONBytesAccessFailed
717          (constructor JSONErrorCode JSONExpectedNumber)))))