1044def jsonParseNumberFraction =
1045 (lambda unrestricted prefix : BytesBuilder .
1046 (lambda unrestricted input : Bytes .
1047 (nat-eliminate
1048 (lambda unrestricted nonEmpty : Nat . (family JSONNumberParseResult))
1049 (app
1050 (lambda unrestricted marker : Byte .
1051 (app
1052 (lambda unrestricted tail : Bytes .
1053 (nat-eliminate
1054 (lambda unrestricted fraction : Nat . (family JSONNumberParseResult))
1055 (jsonParseNumberExponent prefix (bytes-cons marker tail))
1056 (lambda unrestricted fractionPredecessor : Nat .
1057 (lambda unrestricted fractionInduction : (family JSONNumberParseResult) .
1058 (eliminate
1059 JSONDigitSplit
1060 (lambda unrestricted current : (family JSONDigitSplit) .
1061 (family JSONNumberParseResult))
1062 (jsonTakeDigits tail)
1063 (branch
1064 JSONDigitSplitValue
1065 digits
1066 remaining
1067 count
1068 .
1069 (nat-eliminate
1070 (lambda unrestricted nonempty : Nat . (family JSONNumberParseResult))
1071 (jsonNumberFailure
1072 (constructor JSONErrorCode JSONNumberFractionDigitsMissing)
1073 tail)
1074 (lambda unrestricted predecessor : Nat .
1075 (lambda unrestricted induction : (family JSONNumberParseResult) .
1076 (jsonParseNumberExponent
1077 (bytes-builder-append
1078 prefix
1079 (bytes-builder-append (bytes-builder-chunk b".") digits))
1080 remaining)))
1081 count)))))
1082 (byte-equal marker (byte 46))))
1083 (bytes-tail input)))
1084 (bytes-head input))
1085 (lambda unrestricted emptyPredecessor : Nat .
1086 (lambda unrestricted emptyInduction : (family JSONNumberParseResult) .
1087 (jsonParseNumberExponent prefix b"")))
1088 (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.