331def jsonRenderTree =
332 (lambda unrestricted value : (family JSON) .
333 (eliminate
334 JSON
335 (lambda unrestricted current : (family JSON) . (family JSONRenderFragment))
336 value
337 (branch
338 JSONObject
339 members
340 membersInduction
341 .
342 (eliminate
343 JSONRenderFragment
344 (lambda unrestricted current : (family JSONRenderFragment) . (family JSONRenderFragment))
345 membersInduction
346 (branch
347 JSONRenderFragmentSucceeded
348 kind
349 builder
350 count
351 .
352 (nat-eliminate
353 (lambda unrestricted valid : Nat . (family JSONRenderFragment))
354 jsonRenderFailure
355 (lambda unrestricted predecessor : Nat .
356 (lambda unrestricted induction : (family JSONRenderFragment) .
357 (constructor
358 JSONRenderFragment
359 JSONRenderFragmentSucceeded
360 (constructor JSONRenderKind JSONRenderValueKind)
361 (bytes-builder-append
362 (bytes-builder-chunk b"{")
363 (bytes-builder-append builder (bytes-builder-chunk b"}")))
364 (succ zero))))
365 (jsonRenderKindIsObjectMembers kind)))
366 (branch
367 JSONRenderFragmentFailed
368 code
369 .
370 (constructor JSONRenderFragment JSONRenderFragmentFailed code))))
371 (branch
372 JSONObjectEnd
373 .
374 (constructor
375 JSONRenderFragment
376 JSONRenderFragmentSucceeded
377 (constructor JSONRenderKind JSONRenderObjectMembersKind)
378 (bytes-builder-empty)
379 zero))
380 (branch
381 JSONObjectMember
382 key
383 member
384 tail
385 memberInduction
386 tailInduction
387 .
388 (jsonRenderTreePart1 key memberInduction tailInduction))
389 (branch
390 JSONArray
391 values
392 valuesInduction
393 .
394 (eliminate
395 JSONRenderFragment
396 (lambda unrestricted current : (family JSONRenderFragment) . (family JSONRenderFragment))
397 valuesInduction
398 (branch
399 JSONRenderFragmentSucceeded
400 kind
401 builder
402 count
403 .
404 (nat-eliminate
405 (lambda unrestricted valid : Nat . (family JSONRenderFragment))
406 jsonRenderFailure
407 (lambda unrestricted predecessor : Nat .
408 (lambda unrestricted induction : (family JSONRenderFragment) .
409 (constructor
410 JSONRenderFragment
411 JSONRenderFragmentSucceeded
412 (constructor JSONRenderKind JSONRenderValueKind)
413 (bytes-builder-append
414 (bytes-builder-chunk b"[")
415 (bytes-builder-append builder (bytes-builder-chunk b"]")))
416 (succ zero))))
417 (jsonRenderKindIsArrayValues kind)))
418 (branch
419 JSONRenderFragmentFailed
420 code
421 .
422 (constructor JSONRenderFragment JSONRenderFragmentFailed code))))
423 (branch
424 JSONArrayEnd
425 .
426 (constructor
427 JSONRenderFragment
428 JSONRenderFragmentSucceeded
429 (constructor JSONRenderKind JSONRenderArrayValuesKind)
430 (bytes-builder-empty)
431 zero))
432 (branch
433 JSONArrayNext
434 head
435 tail
436 headInduction
437 tailInduction
438 .
439 (eliminate
440 JSONRenderFragment
441 (lambda unrestricted current : (family JSONRenderFragment) . (family JSONRenderFragment))
442 headInduction
443 (branch
444 JSONRenderFragmentSucceeded
445 headKind
446 headBuilder
447 headCount
448 .
449 (jsonRenderTreePart2 tailInduction headKind headBuilder))
450 (branch
451 JSONRenderFragmentFailed
452 code
453 .
454 (constructor JSONRenderFragment JSONRenderFragmentFailed code))))
455 (branch JSONString text . (jsonRenderStringFragment text))
456 (branch
457 JSONNumber
458 number
459 .
460 (eliminate
461 JSONNumberParseResult
462 (lambda unrestricted current : (family JSONNumberParseResult) .
463 (family JSONRenderFragment))
464 (jsonParseNumber number)
465 (branch
466 JSONNumberParsed
467 parsed
468 remaining
469 .
470 (nat-eliminate
471 (lambda unrestricted noTrailing : Nat . (family JSONRenderFragment))
472 jsonRenderFailure
473 (lambda unrestricted predecessor : Nat .
474 (lambda unrestricted induction : (family JSONRenderFragment) .
475 (constructor
476 JSONRenderFragment
477 JSONRenderFragmentSucceeded
478 (constructor JSONRenderKind JSONRenderValueKind)
479 (bytes-builder-chunk parsed)
480 (succ zero))))
481 (naturalIsZero (bytes-length remaining))))
482 (branch JSONNumberParseFailed code remaining . jsonRenderFailure)))
483 (branch
484 JSONBoolean
485 boolean
486 .
487 (constructor
488 JSONRenderFragment
489 JSONRenderFragmentSucceeded
490 (constructor JSONRenderKind JSONRenderValueKind)
491 (nat-eliminate
492 (lambda unrestricted current : Nat . BytesBuilder)
493 (bytes-builder-chunk b"false")
494 (lambda unrestricted predecessor : Nat .
495 (lambda unrestricted induction : BytesBuilder .
496 (bytes-builder-chunk b"true")))
497 boolean)
498 (succ zero)))
499 (branch
500 JSONNull
501 .
502 (constructor
503 JSONRenderFragment
504 JSONRenderFragmentSucceeded
505 (constructor JSONRenderKind JSONRenderValueKind)
506 (bytes-builder-chunk b"null")
507 (succ zero)))))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.