def reverse_source_array_whole

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

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

476def reverse_source_array_whole(+head: J.Value,
477                               +tail: List<&2, J.Value>) -> {reverse_source_task(J.Arr{head <> tail}, RenderWhole{}) == List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}), List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> Nil{})) : List<&2, J.Lexeme>}:
478    Equal.trans(List<&2, J.Lexeme>,
479        reverse_source_task(J.Arr{head <> tail}, RenderWhole{}),
480        List.reverse(&2, J.Lexeme, List.append(&2, J.Lexeme,
481            J.Punctuation{'['} <> J.source(head, False{}, Nil{}), J.source(J.Arr{tail}, True{}, Nil{}))),
482        List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}),
483            List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> Nil{})),
484        Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => List.reverse(&2, J.Lexeme, items),
485            J.source(J.Arr{head <> tail}, False{}, Nil{}),
486            List.append(&2, J.Lexeme, J.Punctuation{'['} <> J.source(head, False{}, Nil{}), J.source(J.Arr{tail}, True{}, Nil{})),
487            Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => J.Punctuation{'['} <> items,
488                J.source(head, False{}, J.source(J.Arr{tail}, True{}, Nil{})),
489                List.append(&2, J.Lexeme, J.source(head, False{}, Nil{}), J.source(J.Arr{tail}, True{}, Nil{})),
490                source_append(head, False{}, Nil{}, J.source(J.Arr{tail}, True{}, Nil{})))),
491        Equal.trans(List<&2, J.Lexeme>,
492            List.reverse(&2, J.Lexeme, List.append(&2, J.Lexeme,
493                J.Punctuation{'['} <> J.source(head, False{}, Nil{}), J.source(J.Arr{tail}, True{}, Nil{}))),
494            List.append(&2, J.Lexeme,
495                List.reverse(&2, J.Lexeme, J.source(J.Arr{tail}, True{}, Nil{})),
496                List.reverse(&2, J.Lexeme, J.Punctuation{'['} <> J.source(head, False{}, Nil{}))),
497            List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}),
498                List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> Nil{})),
499            LP.reverse_append(J.Lexeme, J.Punctuation{'['} <> J.source(head, False{}, Nil{}), J.source(J.Arr{tail}, True{}, Nil{})),
500            Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}), items),
501                List.reverse(&2, J.Lexeme, J.Punctuation{'['} <> J.source(head, False{}, Nil{})),
502                List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> Nil{}),
503                LP.reverse_cons(J.Lexeme, J.Punctuation{'['}, J.source(head, False{}, Nil{})))))