def reverse_source_array_members_after_separator

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

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

569def reverse_source_array_members_after_separator(+head: J.Value,
570                                                 +tail: List<&2, J.Value>) -> {reverse_source_task(J.Arr{head <> tail}, RenderMembers{}) == List.append(&2, J.Lexeme, reverse_source_task(J.Arr{head <> tail}, RenderAfterSeparator{}), J.Punctuation{','} <> Nil{}) : List<&2, J.Lexeme>}:
571    Equal.trans(List<&2, J.Lexeme>,
572        reverse_source_task(J.Arr{head <> tail}, RenderMembers{}),
573        List.reverse(&2, J.Lexeme, J.Punctuation{','} <> source_after_separator(J.Arr{head <> tail}, Nil{})),
574        List.append(&2, J.Lexeme, reverse_source_task(J.Arr{head <> tail}, RenderAfterSeparator{}),
575            J.Punctuation{','} <> Nil{}),
576        Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => List.reverse(&2, J.Lexeme, items),
577            J.source(J.Arr{head <> tail}, True{}, Nil{}),
578            J.Punctuation{','} <> source_after_separator(J.Arr{head <> tail}, Nil{}),
579            {==}),
580        LP.reverse_cons(J.Lexeme, J.Punctuation{','}, source_after_separator(J.Arr{head <> tail}, Nil{})))