JSONSourceProof.lex_simple_array_whole: def of qasim-bend-kit@0.1.0.2 Import: import qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend as JSONSourceProof Lines 1349-1380 of qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&start_line=1349&end_line=1380 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_LexWhitespaceProof.bend as W import qasim-bend-kit@0.1.0.2/proof/JSON_ListProof.bend as LP def lex_simple_array_whole(+values: List<&2, SimpleValue>) -> {J.lex_scan(J.render(J.Arr{simple_values(values)}, False{}, SNil{}), J.Outside{}, SNil{}, Nil{}) == J.source(J.Arr{simple_values(values)}, False{}, Nil{}) : List<&2, J.Lexeme>}: Equal.trans(List<&2, J.Lexeme>, J.lex_scan(J.render(J.Arr{simple_values(values)}, False{}, SNil{}), J.Outside{}, SNil{}, Nil{}), J.lex_scan(render_after_separator(J.Arr{simple_values(values)}, SNil{}), J.Outside{}, SNil{}, J.Punctuation{'['} <> Nil{}), J.source(J.Arr{simple_values(values)}, False{}, Nil{}), Equal.trans(List<&2, J.Lexeme>, J.lex_scan(J.render(J.Arr{simple_values(values)}, False{}, SNil{}), J.Outside{}, SNil{}, Nil{}), J.lex_scan("[" ++ render_after_separator(J.Arr{simple_values(values)}, SNil{}), J.Outside{}, SNil{}, Nil{}), J.lex_scan(render_after_separator(J.Arr{simple_values(values)}, SNil{}), J.Outside{}, SNil{}, J.Punctuation{'['} <> Nil{}), Equal.cong(String, List<&2, J.Lexeme>, text => J.lex_scan(text, J.Outside{}, SNil{}, Nil{}), J.render(J.Arr{simple_values(values)}, False{}, SNil{}), "[" ++ render_after_separator(J.Arr{simple_values(values)}, SNil{}), render_array_whole_after_separator(simple_values(values), SNil{})), W.scan_punctuation_char('[', render_after_separator(J.Arr{simple_values(values)}, SNil{}), SNil{}, Nil{}, {==})), Equal.trans(List<&2, J.Lexeme>, J.lex_scan(render_after_separator(J.Arr{simple_values(values)}, SNil{}), J.Outside{}, SNil{}, J.Punctuation{'['} <> Nil{}), J.lex_scan(SNil{}, J.Outside{}, SNil{}, List.append(&2, J.Lexeme, reverse_source_task(J.Arr{simple_values(values)}, RenderAfterSeparator{}), J.Punctuation{'['} <> Nil{})), J.source(J.Arr{simple_values(values)}, False{}, Nil{}), lex_simple_array_after_separator_end(values, J.Punctuation{'['} <> Nil{}), Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SNil{}, J.Outside{}, SNil{}, List.append(&2, J.Lexeme, reverse_source_task(J.Arr{simple_values(values)}, RenderAfterSeparator{}), J.Punctuation{'['} <> Nil{})), J.lex_scan(SNil{}, J.Outside{}, SNil{}, reverse_source_task(J.Arr{simple_values(values)}, RenderWhole{})), J.source(J.Arr{simple_values(values)}, False{}, Nil{}), Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => J.lex_scan(SNil{}, J.Outside{}, SNil{}, items), List.append(&2, J.Lexeme, reverse_source_task(J.Arr{simple_values(values)}, RenderAfterSeparator{}), J.Punctuation{'['} <> Nil{}), reverse_source_task(J.Arr{simple_values(values)}, RenderWhole{}), Equal.sym(List<&2, J.Lexeme>, reverse_source_task(J.Arr{simple_values(values)}, RenderWhole{}), List.append(&2, J.Lexeme, reverse_source_task(J.Arr{simple_values(values)}, RenderAfterSeparator{}), J.Punctuation{'['} <> Nil{}), reverse_source_array_after_separator_whole_list(simple_values(values)))), LP.reverse_twice(J.Lexeme, J.source(J.Arr{simple_values(values)}, False{}, Nil{}))))) Uses (25): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Char https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String.append https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=LexMode https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=Lexeme https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=Value https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=lex_scan https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=render https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=source https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_LexWhitespaceProof.bend&name=scan_punctuation_char https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_ListProof.bend&name=reverse_twice https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=RenderMode https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=SimpleValue https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=lex_simple_array_after_separator_end https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=render_after_separator https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=render_array_whole_after_separator https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=reverse_source_array_after_separator_whole_list https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=reverse_source_task https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=simple_values