985def jsonIntegerFromBytes =
986 (lambda unrestricted input : Bytes .
987 (bytes-eliminate
988 (lambda unrestricted current : Bytes . (family JSONIntegerAccessResult))
989 (constructor
990 JSONIntegerAccessResult
991 JSONIntegerAccessFailed
992 (constructor JSONErrorCode JSONExpectedInteger))
993 (lambda unrestricted head : Byte .
994 (lambda unrestricted tail : Bytes .
995 (lambda unrestricted tailInduction : (family JSONIntegerAccessResult) .
996 (app
997 (lambda unrestricted negative : Nat .
998 (app
999 (lambda unrestricted digits : Bytes .
1000 (eliminate
1001 JSONIntegerFoldResult
1002 (lambda unrestricted current : (family JSONIntegerFoldResult) .
1003 (family JSONIntegerAccessResult))
1004 (jsonIntegerFold digits)
1005 (branch
1006 JSONIntegerFoldSucceeded
1007 magnitude
1008 count
1009 .
1010 (nat-eliminate
1011 (lambda unrestricted supported : Nat . (family JSONIntegerAccessResult))
1012 (constructor
1013 JSONIntegerAccessResult
1014 JSONIntegerAccessFailed
1015 (constructor JSONErrorCode JSONNumericRangeUnsupported))
1016 (lambda unrestricted supportedPredecessor : Nat .
1017 (lambda unrestricted supportedInduction : (family JSONIntegerAccessResult) .
1018 (nat-eliminate
1019 (lambda unrestricted nonempty : Nat .
1020 (family JSONIntegerAccessResult))
1021 (constructor
1022 JSONIntegerAccessResult
1023 JSONIntegerAccessFailed
1024 (constructor JSONErrorCode JSONExpectedInteger))
1025 (lambda unrestricted predecessor : Nat .
1026 (lambda unrestricted induction : (family JSONIntegerAccessResult) .
1027 (constructor
1028 JSONIntegerAccessResult
1029 JSONIntegerAccessSucceeded
1030 (constructor
1031 JSONInteger
1032 JSONIntegerValue
1033 (nat-eliminate
1034 (lambda unrestricted zeroMagnitude : Nat . Nat)
1035 negative
1036 (lambda unrestricted magnitudePredecessor : Nat .
1037 (lambda unrestricted magnitudeInduction : Nat . zero))
1038 (naturalIsZero magnitude))
1039 magnitude))))
1040 count)))
1041 (jsonIntegerDigitsFitInt64 digits)))
1042 (branch
1043 JSONIntegerFoldFailed
1044 .
1045 (constructor
1046 JSONIntegerAccessResult
1047 JSONIntegerAccessFailed
1048 (constructor JSONErrorCode JSONExpectedInteger)))))
1049 (nat-eliminate
1050 (lambda unrestricted signed : Nat . Bytes)
1051 input
1052 (lambda unrestricted predecessor : Nat .
1053 (lambda unrestricted induction : Bytes . tail))
1054 negative)))
1055 (byte-equal head (byte 45))))))
1056 input))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.