Data.JSON

670def jsonParseEscape =
671  (lambda unrestricted continuation : (pi unrestricted input : Bytes . (family JSONStringParseResult)) .
672    (lambda unrestricted input : Bytes .
673      (nat-eliminate
674        (lambda unrestricted nonEmpty : Nat . (family JSONStringParseResult))
675        (app
676          (lambda unrestricted escaped : Byte .
677            (app
678              (lambda unrestricted remaining : Bytes .
679                (nat-eliminate
680                  (lambda unrestricted quote : Nat . (family JSONStringParseResult))
681                  (nat-eliminate
682                    (lambda unrestricted slash : Nat . (family JSONStringParseResult))
683                    (nat-eliminate
684                      (lambda unrestricted solidus : Nat . (family JSONStringParseResult))
685                      (nat-eliminate
686                        (lambda unrestricted backspace : Nat . (family JSONStringParseResult))
687                        (nat-eliminate
688                          (lambda unrestricted formFeed : Nat . (family JSONStringParseResult))
689                          (nat-eliminate
690                            (lambda unrestricted newline : Nat . (family JSONStringParseResult))
691                            (nat-eliminate
692                              (lambda unrestricted carriage : Nat . (family JSONStringParseResult))
693                              (nat-eliminate
694                                (lambda unrestricted tab : Nat . (family JSONStringParseResult))
695                                (nat-eliminate
696                                  (lambda unrestricted unicode : Nat .
697                                    (family JSONStringParseResult))
698                                  (jsonStringFailure
699                                    (constructor JSONErrorCode JSONEscapeInvalid)
700                                    input)
701                                  (lambda unrestricted predecessor : Nat .
702                                    (lambda unrestricted induction : (family JSONStringParseResult) .
703                                      (jsonParseUnicodeEscape continuation remaining)))
704                                  (byte-equal escaped (byte 117)))
705                                (lambda unrestricted predecessor : Nat .
706                                  (lambda unrestricted induction : (family JSONStringParseResult) .
707                                    (jsonStringPrepend (bytes 9) (continuation remaining))))
708                                (byte-equal escaped (byte 116)))
709                              (lambda unrestricted predecessor : Nat .
710                                (lambda unrestricted induction : (family JSONStringParseResult) .
711                                  (jsonStringPrepend (bytes 13) (continuation remaining))))
712                              (byte-equal escaped (byte 114)))
713                            (lambda unrestricted predecessor : Nat .
714                              (lambda unrestricted induction : (family JSONStringParseResult) .
715                                (jsonStringPrepend (bytes 10) (continuation remaining))))
716                            (byte-equal escaped (byte 110)))
717                          (lambda unrestricted predecessor : Nat .
718                            (lambda unrestricted induction : (family JSONStringParseResult) .
719                              (jsonStringPrepend (bytes 12) (continuation remaining))))
720                          (byte-equal escaped (byte 102)))
721                        (lambda unrestricted predecessor : Nat .
722                          (lambda unrestricted induction : (family JSONStringParseResult) .
723                            (jsonStringPrepend (bytes 8) (continuation remaining))))
724                        (byte-equal escaped (byte 98)))
725                      (lambda unrestricted predecessor : Nat .
726                        (lambda unrestricted induction : (family JSONStringParseResult) .
727                          (jsonStringPrepend b"/" (continuation remaining))))
728                      (byte-equal escaped (byte 47)))
729                    (lambda unrestricted predecessor : Nat .
730                      (lambda unrestricted induction : (family JSONStringParseResult) .
731                        (jsonStringPrepend b"\\" (continuation remaining))))
732                    (byte-equal escaped (byte 92)))
733                  (lambda unrestricted predecessor : Nat .
734                    (lambda unrestricted induction : (family JSONStringParseResult) .
735                      (jsonStringPrepend b"\"" (continuation remaining))))
736                  (byte-equal escaped (byte 34))))
737              (bytes-tail input)))
738          (bytes-head input))
739        (lambda unrestricted emptyPredecessor : Nat .
740          (lambda unrestricted emptyInduction : (family JSONStringParseResult) .
741            (jsonStringFailure (constructor JSONErrorCode JSONStringUnterminated) input)))
742        (naturalIsZero (bytes-length input)))))