1090def jsonParseNumberUnsigned =
1091 (lambda unrestricted prefix : BytesBuilder .
1092 (lambda unrestricted input : Bytes .
1093 (nat-eliminate
1094 (lambda unrestricted nonEmpty : Nat . (family JSONNumberParseResult))
1095 (app
1096 (lambda unrestricted first : Byte .
1097 (app
1098 (lambda unrestricted tail : Bytes .
1099 (nat-eliminate
1100 (lambda unrestricted zeroDigit : Nat . (family JSONNumberParseResult))
1101 (nat-eliminate
1102 (lambda unrestricted nonzero : Nat . (family JSONNumberParseResult))
1103 (jsonNumberFailure (constructor JSONErrorCode JSONNumberIntegerInvalid) input)
1104 (lambda unrestricted predecessor : Nat .
1105 (lambda unrestricted induction : (family JSONNumberParseResult) .
1106 (eliminate
1107 JSONDigitSplit
1108 (lambda unrestricted current : (family JSONDigitSplit) .
1109 (family JSONNumberParseResult))
1110 (jsonTakeDigits tail)
1111 (branch
1112 JSONDigitSplitValue
1113 digits
1114 remaining
1115 count
1116 .
1117 (jsonParseNumberFraction
1118 (bytes-builder-append
1119 prefix
1120 (bytes-builder-append
1121 (bytes-builder-chunk (bytes-cons first b""))
1122 digits))
1123 remaining)))))
1124 (jsonByteIsNonzeroDigit first))
1125 (lambda unrestricted predecessor : Nat .
1126 (lambda unrestricted induction : (family JSONNumberParseResult) .
1127 (jsonParseNumberFraction
1128 (bytes-builder-append prefix (bytes-builder-chunk b"0"))
1129 tail)))
1130 (byte-equal first (byte 48))))
1131 (bytes-tail input)))
1132 (bytes-head input))
1133 (lambda unrestricted emptyPredecessor : Nat .
1134 (lambda unrestricted emptyInduction : (family JSONNumberParseResult) .
1135 (jsonNumberFailure (constructor JSONErrorCode JSONNumberIntegerInvalid) input)))
1136 (naturalIsZero (bytes-length 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.