def reverse_source_object_members_after_separator

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

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

462def reverse_source_object_members_after_separator(+key: String,
463                                                  +value: J.Value,
464                                                  +tail: List<&2, Sigma<&2, &2, String, key => J.Value>>) -> {reverse_source_task(J.Obj{(key, value) <> tail}, RenderMembers{}) == List.append(&2, J.Lexeme, reverse_source_task(J.Obj{(key, value) <> tail}, RenderAfterSeparator{}), J.Punctuation{','} <> Nil{}) : List<&2, J.Lexeme>}:
465    Equal.trans(List<&2, J.Lexeme>,
466        reverse_source_task(J.Obj{(key, value) <> tail}, RenderMembers{}),
467        List.reverse(&2, J.Lexeme, J.Punctuation{','} <> source_after_separator(J.Obj{(key, value) <> tail}, Nil{})),
468        List.append(&2, J.Lexeme, reverse_source_task(J.Obj{(key, value) <> tail}, RenderAfterSeparator{}),
469            J.Punctuation{','} <> Nil{}),
470        Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => List.reverse(&2, J.Lexeme, items),
471            J.source(J.Obj{(key, value) <> tail}, True{}, Nil{}),
472            J.Punctuation{','} <> source_after_separator(J.Obj{(key, value) <> tail}, Nil{}),
473            {==}),
474        LP.reverse_cons(J.Lexeme, J.Punctuation{','}, source_after_separator(J.Obj{(key, value) <> tail}, Nil{})))