def render_object
qasim-bend-kit@0.1.0.2 · proof/JSON_RenderLexProof.bend:462
import qasim-bend-kit@0.1.0.2/proof/JSON_RenderLexProof.bend as JSONRenderLexProof
import Base
import qasim-bend-kit@0.1.0.2/libs/JSON.bend as J
import qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend as SP
462def render_object(+key: String,
463 +head: J.Value,
464 +tail: List<&2, Sigma<&2, &2, String, k => J.Value>>, +mode: SP.RenderMode, +boundary: Boundary, +acc: List<&2,
465 J.Lexeme>) -> {SP.render_task(J.Obj{(key, head) <> tail}, mode, boundary_text(boundary)) == prefix_text(ObjectKind{}, mode, J.render_object_field(SNil{}, key, SP.render_task(head, SP.RenderWhole{}, boundary_text(object_continuation(tail, boundary))))) : String}:
466 match mode:
467 case SP.RenderWhole{}:
468 Equal.cong(String, String,
469 x => prefix_text(ObjectKind{}, SP.RenderWhole{}, J.render_object_field(SNil{}, key, SP.render_task(head, SP.RenderWhole{}, x))),
470 SP.render_task(J.Obj{tail}, SP.RenderMembers{}, boundary_text(boundary)),
471 boundary_text(object_continuation(tail, boundary)),
472 object_continuation_text(tail, boundary))
473 case SP.RenderMembers{}:
474 Equal.cong(String, String,
475 x => prefix_text(ObjectKind{}, SP.RenderMembers{}, J.render_object_field(SNil{}, key, SP.render_task(head, SP.RenderWhole{}, x))),
476 SP.render_task(J.Obj{tail}, SP.RenderMembers{}, boundary_text(boundary)),
477 boundary_text(object_continuation(tail, boundary)),
478 object_continuation_text(tail, boundary))
479 case SP.RenderAfterSeparator{}:
480 Equal.cong(String, String,
481 x => prefix_text(ObjectKind{}, SP.RenderAfterSeparator{}, J.render_object_field(SNil{}, key, SP.render_task(head, SP.RenderWhole{}, x))),
482 SP.render_task(J.Obj{tail}, SP.RenderMembers{}, boundary_text(boundary)),
483 boundary_text(object_continuation(tail, boundary)),
484 object_continuation_text(tail, boundary))