1138def jsonParseNumber =
1139 (lambda unrestricted input : Bytes .
1140 (nat-eliminate
1141 (lambda unrestricted nonEmpty : Nat . (family JSONNumberParseResult))
1142 (app
1143 (lambda unrestricted head : Byte .
1144 (app
1145 (lambda unrestricted tail : Bytes .
1146 (nat-eliminate
1147 (lambda unrestricted negative : Nat . (family JSONNumberParseResult))
1148 (jsonParseNumberUnsigned (bytes-builder-empty) input)
1149 (lambda unrestricted predecessor : Nat .
1150 (lambda unrestricted induction : (family JSONNumberParseResult) .
1151 (jsonParseNumberUnsigned (bytes-builder-chunk b"-") tail)))
1152 (byte-equal head (byte 45))))
1153 (bytes-tail input)))
1154 (bytes-head input))
1155 (lambda unrestricted emptyPredecessor : Nat .
1156 (lambda unrestricted emptyInduction : (family JSONNumberParseResult) .
1157 (jsonNumberFailure (constructor JSONErrorCode JSONNumberIntegerInvalid) input)))
1158 (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.