Part of `jsonRenderTree`, lifted out to keep it inside the §28.3 size and
nesting limits; the parameters are the locals it still needs.
291def jsonRenderTreePart2 =
292 (lambda unrestricted tailInduction : (family JSONRenderFragment) .
293 (lambda unrestricted headKind : (family JSONRenderKind) .
294 (lambda unrestricted headBuilder : BytesBuilder .
295 (eliminate
296 JSONRenderFragment
297 (lambda unrestricted current : (family JSONRenderFragment) . (family JSONRenderFragment))
298 tailInduction
299 (branch
300 JSONRenderFragmentSucceeded
301 tailKind
302 tailBuilder
303 tailCount
304 .
305 (nat-eliminate
306 (lambda unrestricted validHead : Nat . (family JSONRenderFragment))
307 jsonRenderFailure
308 (lambda unrestricted headPredecessor : Nat .
309 (lambda unrestricted headRoleInduction : (family JSONRenderFragment) .
310 (nat-eliminate
311 (lambda unrestricted validTail : Nat . (family JSONRenderFragment))
312 jsonRenderFailure
313 (lambda unrestricted tailPredecessor : Nat .
314 (lambda unrestricted tailRoleInduction : (family JSONRenderFragment) .
315 (constructor
316 JSONRenderFragment
317 JSONRenderFragmentSucceeded
318 (constructor JSONRenderKind JSONRenderArrayValuesKind)
319 (bytes-builder-append
320 headBuilder
321 (bytes-builder-append (jsonRenderCommaBefore tailCount) tailBuilder))
322 (succ tailCount))))
323 (jsonRenderKindIsArrayValues tailKind))))
324 (jsonRenderKindIsValue headKind)))
325 (branch
326 JSONRenderFragmentFailed
327 code
328 .
329 (constructor JSONRenderFragment JSONRenderFragmentFailed 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.