Part of `jsonAuditTreeWithTokenLimits`, lifted out to keep it inside the §28.3 size and
nesting limits; the parameters are the locals it still needs.
2239def jsonAuditTreeWithTokenLimitsPart3 =
2240 (lambda unrestricted number : Bytes .
2241 (lambda unrestricted boundedPredecessor : Nat .
2242 (lambda unrestricted boundedInduction : (family JSONTreeAuditResult) .
2243 (eliminate
2244 JSONNumberParseResult
2245 (lambda unrestricted current : (family JSONNumberParseResult) .
2246 (family JSONTreeAuditResult))
2247 (jsonParseNumber number)
2248 (branch
2249 JSONNumberParsed
2250 parsed
2251 remaining
2252 .
2253 (nat-eliminate
2254 (lambda unrestricted complete : Nat . (family JSONTreeAuditResult))
2255 (jsonTreeAuditFailure (constructor JSONErrorCode JSONMalformedTree))
2256 (lambda unrestricted predecessor : Nat .
2257 (lambda unrestricted induction : (family JSONTreeAuditResult) .
2258 (constructor
2259 JSONTreeAuditResult
2260 JSONTreeAuditSucceeded
2261 (constructor JSONTreeKind JSONTreeValueKind)
2262 (jsonCountsNumber (bytes-length number))
2263 (succ zero)
2264 zero)))
2265 (naturalIsZero (bytes-length remaining))))
2266 (branch JSONNumberParseFailed code remaining . (jsonTreeAuditFailure code))))))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.