One audit condition: the result when `flag` holds, else the failure `code`.
The container audits chain these so that each rejected condition reports
its own code (a malformed tree, a duplicate key, a key past the string
limit, a container past the entry limit) instead of one shared code.
2106def jsonAuditGate =
2107 (lambda unrestricted flag : Nat .
2108 (lambda unrestricted code : (family JSONErrorCode) .
2109 (lambda unrestricted otherwise : (family JSONTreeAuditResult) .
2110 (nat-eliminate
2111 (lambda unrestricted valid : Nat . (family JSONTreeAuditResult))
2112 (jsonTreeAuditFailure code)
2113 (lambda unrestricted predecessor : Nat .
2114 (lambda unrestricted induction : (family JSONTreeAuditResult) . otherwise))
2115 flag))))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.