509def jsonRenderUnchecked =
510 (lambda unrestricted value : (family JSON) .
511 (eliminate
512 JSONRenderFragment
513 (lambda unrestricted current : (family JSONRenderFragment) . (family JSONRenderResult))
514 (jsonRenderTree value)
515 (branch
516 JSONRenderFragmentSucceeded
517 kind
518 builder
519 count
520 .
521 (nat-eliminate
522 (lambda unrestricted valid : Nat . (family JSONRenderResult))
523 (constructor
524 JSONRenderResult
525 JSONRenderFailed
526 (constructor JSONErrorCode JSONMalformedTree))
527 (lambda unrestricted predecessor : Nat .
528 (lambda unrestricted induction : (family JSONRenderResult) .
529 (constructor JSONRenderResult JSONRendered (bytes-builder-build builder))))
530 (jsonRenderKindIsValue kind)))
531 (branch JSONRenderFragmentFailed code . (constructor JSONRenderResult JSONRenderFailed 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.