def reverse_source_colon_value_tail

qasim-bend-kit@0.1.0.2 · proof/JSON_SourceProof.bend:380

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_ListProof.bend as LP

380def reverse_source_colon_value_tail(+value: J.Value,
381                                    +tail: List<&2, Sigma<&2, &2, String, key => J.Value>>) -> {List.reverse(&2, J.Lexeme, J.Punctuation{':'} <> J.source(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))) == List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}), List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> Nil{})) : List<&2, J.Lexeme>}:
382    Equal.trans(List<&2, J.Lexeme>,
383        List.reverse(&2, J.Lexeme, J.Punctuation{':'} <> J.source(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))),
384        List.append(&2, J.Lexeme,
385            List.reverse(&2, J.Lexeme, J.source(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))),
386            J.Punctuation{':'} <> Nil{}),
387        List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}),
388            List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> Nil{})),
389        LP.reverse_cons(J.Lexeme, J.Punctuation{':'}, J.source(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))),
390        Equal.trans(List<&2, J.Lexeme>,
391            List.append(&2, J.Lexeme,
392                List.reverse(&2, J.Lexeme, J.source(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))),
393                J.Punctuation{':'} <> Nil{}),
394            List.append(&2, J.Lexeme,
395                List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}), reverse_source_task(value, RenderWhole{})),
396                J.Punctuation{':'} <> Nil{}),
397            List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}),
398                List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> Nil{})),
399            Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs =>
400                List.append(&2, J.Lexeme, xs, J.Punctuation{':'} <> Nil{}),
401                List.reverse(&2, J.Lexeme, J.source(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))),
402                List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}), reverse_source_task(value, RenderWhole{})),
403                reverse_source_suffix(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))),
404            LP.append_assoc(J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}),
405                reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> Nil{})))