536def renderJSONObservedWithLimits =
537 (lambda unrestricted limits : (family JSONLimits) .
538 (lambda unrestricted value : (family JSON) .
539 (eliminate
540 JSONLimits
541 (lambda unrestricted current : (family JSONLimits) . (family JSONObservedRenderResult))
542 limits
543 (branch
544 JSONLimitsValue
545 maximumInputBytes
546 maximumDepth
547 maximumStringBytes
548 maximumNumberBytes
549 maximumContainerEntries
550 maximumOutputBytes
551 .
552 (eliminate
553 JSONTreeAuditResult
554 (lambda unrestricted current : (family JSONTreeAuditResult) .
555 (family JSONObservedRenderResult))
556 (jsonAuditTreeWithTokenLimits
557 maximumStringBytes
558 maximumNumberBytes
559 maximumContainerEntries
560 value)
561 (branch
562 JSONTreeAuditSucceeded
563 kind
564 counts
565 depth
566 sequenceCount
567 .
568 (nat-eliminate
569 (lambda unrestricted valueKind : Nat . (family JSONObservedRenderResult))
570 (constructor
571 JSONObservedRenderResult
572 JSONObservedRenderFailed
573 (constructor JSONErrorCode JSONMalformedTree)
574 (constructor JSONRenderTelemetry JSONRenderTelemetryValue counts depth zero))
575 (lambda unrestricted kindPredecessor : Nat .
576 (lambda unrestricted kindInduction : (family JSONObservedRenderResult) .
577 (nat-eliminate
578 (lambda unrestricted depthBounded : Nat . (family JSONObservedRenderResult))
579 (constructor
580 JSONObservedRenderResult
581 JSONObservedRenderFailed
582 (constructor JSONErrorCode JSONDepthLimitExceeded)
583 (constructor JSONRenderTelemetry JSONRenderTelemetryValue counts depth zero))
584 (lambda unrestricted depthPredecessor : Nat .
585 (lambda unrestricted depthInduction : (family JSONObservedRenderResult) .
586 (eliminate
587 JSONRenderResult
588 (lambda unrestricted current : (family JSONRenderResult) .
589 (family JSONObservedRenderResult))
590 (jsonRenderUnchecked value)
591 (branch
592 JSONRendered
593 output
594 .
595 (nat-eliminate
596 (lambda unrestricted outputBounded : Nat .
597 (family JSONObservedRenderResult))
598 (constructor
599 JSONObservedRenderResult
600 JSONObservedRenderFailed
601 (constructor JSONErrorCode JSONOutputLimitExceeded)
602 (constructor
603 JSONRenderTelemetry
604 JSONRenderTelemetryValue
605 counts
606 depth
607 (bytes-length output)))
608 (lambda unrestricted outputPredecessor : Nat .
609 (lambda unrestricted outputInduction : (family JSONObservedRenderResult) .
610 (constructor
611 JSONObservedRenderResult
612 JSONObservedRendered
613 output
614 (constructor
615 JSONRenderTelemetry
616 JSONRenderTelemetryValue
617 counts
618 depth
619 (bytes-length output)))))
620 (jsonBoundAllows maximumOutputBytes (bytes-length output))))
621 (branch
622 JSONRenderFailed
623 code
624 .
625 (constructor
626 JSONObservedRenderResult
627 JSONObservedRenderFailed
628 code
629 (constructor
630 JSONRenderTelemetry
631 JSONRenderTelemetryValue
632 counts
633 depth
634 zero))))))
635 (jsonBoundAllows maximumDepth depth))))
636 (jsonTreeKindIsValue kind)))
637 (branch
638 JSONTreeAuditFailed
639 code
640 .
641 (constructor
642 JSONObservedRenderResult
643 JSONObservedRenderFailed
644 code
645 jsonEmptyRenderTelemetry)))))))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.