Part of `jsonAuditTreeWithTokenLimits`, lifted out to keep it inside the §28.3 size and
nesting limits; the parameters are the locals it still needs.
2193def jsonAuditTreeWithTokenLimitsPart2 =
2194 (lambda unrestricted maximumContainerEntries : (family JSONBound) .
2195 (lambda unrestricted headInduction : (family JSONTreeAuditResult) .
2196 (lambda unrestricted tailInduction : (family JSONTreeAuditResult) .
2197 (eliminate
2198 JSONTreeAuditResult
2199 (lambda unrestricted current : (family JSONTreeAuditResult) .
2200 (family JSONTreeAuditResult))
2201 headInduction
2202 (branch
2203 JSONTreeAuditSucceeded
2204 headKind
2205 headCounts
2206 headDepth
2207 headSequence
2208 .
2209 (eliminate
2210 JSONTreeAuditResult
2211 (lambda unrestricted current : (family JSONTreeAuditResult) .
2212 (family JSONTreeAuditResult))
2213 tailInduction
2214 (branch
2215 JSONTreeAuditSucceeded
2216 tailKind
2217 tailCounts
2218 tailDepth
2219 tailSequence
2220 .
2221 (jsonAuditGate
2222 (jsonFlagAnd (jsonTreeKindIsValue headKind) (jsonTreeKindIsArrayValues tailKind))
2223 (constructor JSONErrorCode JSONMalformedTree)
2224 (jsonAuditGate
2225 (jsonBoundAllows maximumContainerEntries (succ tailSequence))
2226 (constructor JSONErrorCode JSONContainerLimitExceeded)
2227 (constructor
2228 JSONTreeAuditResult
2229 JSONTreeAuditSucceeded
2230 (constructor JSONTreeKind JSONTreeArrayValuesKind)
2231 (jsonCountsAdd jsonCountsArrayElement (jsonCountsAdd headCounts tailCounts))
2232 (jsonNaturalMaximum headDepth tailDepth)
2233 (succ tailSequence)))))
2234 (branch JSONTreeAuditFailed code . (jsonTreeAuditFailure code))))
2235 (branch JSONTreeAuditFailed code . (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.