def reverse_source_array_after_separator_whole

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

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

538def reverse_source_array_after_separator_whole(+head: J.Value,
539                                               +tail: List<&2, J.Value>) -> {reverse_source_task(J.Arr{head <> tail}, RenderWhole{}) == List.append(&2, J.Lexeme, reverse_source_task(J.Arr{head <> tail}, RenderAfterSeparator{}), J.Punctuation{'['} <> Nil{}) : List<&2, J.Lexeme>}:
540    Equal.trans(List<&2, J.Lexeme>,
541        reverse_source_task(J.Arr{head <> tail}, RenderWhole{}),
542        List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}),
543            List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> Nil{})),
544        List.append(&2, J.Lexeme, reverse_source_task(J.Arr{head <> tail}, RenderAfterSeparator{}), J.Punctuation{'['} <> Nil{}),
545        reverse_source_array_whole(head, tail),
546        Equal.trans(List<&2, J.Lexeme>,
547            List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}),
548                List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> Nil{})),
549            List.append(&2, J.Lexeme,
550                List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}), reverse_source_task(head, RenderWhole{})),
551                J.Punctuation{'['} <> Nil{}),
552            List.append(&2, J.Lexeme, reverse_source_task(J.Arr{head <> tail}, RenderAfterSeparator{}), J.Punctuation{'['} <> Nil{}),
553            Equal.sym(List<&2, J.Lexeme>,
554                List.append(&2, J.Lexeme,
555                    List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}), reverse_source_task(head, RenderWhole{})),
556                    J.Punctuation{'['} <> Nil{}),
557                List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}),
558                    List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> Nil{})),
559                LP.append_assoc(J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}),
560                    reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> Nil{})),
561            Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items =>
562                List.append(&2, J.Lexeme, items, J.Punctuation{'['} <> Nil{}),
563                List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}), reverse_source_task(head, RenderWhole{})),
564                reverse_source_task(J.Arr{head <> tail}, RenderAfterSeparator{}),
565                Equal.sym(List<&2, J.Lexeme>, reverse_source_task(J.Arr{head <> tail}, RenderAfterSeparator{}),
566                    List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}), reverse_source_task(head, RenderWhole{})),
567                    reverse_source_array_after_separator(head, tail)))))