Source/Packages

Data.JSONRender

packages/foundation/standard/src/Data/JSONRender.alpha

669 lines45 declarations25.9 KiBSHA-256 62bf45d6adaa

def · lines 509–531

jsonRenderUnchecked

Full file
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.