JSONSourceProof.lex_array_after_separator_single: 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 1088-1115 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=1088&end_line=1115

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

def lex_array_after_separator_single(+head: J.Value,
                                     +punctuation: Char,
                                     +suffix: String,
                                     +acc: List<&2, J.Lexeme>,
                                     action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction},
                                     head_lex: {J.lex_scan(render_task(head, RenderWhole{}, "]" ++ (SCon{punctuation, SNil{}} ++ suffix)), J.Outside{}, SNil{}, acc) == J.lex_scan(SCon{punctuation, SNil{}} ++ suffix, J.Outside{}, SNil{}, J.Punctuation{']'} <> List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)) : List<&2,
                                     J.Lexeme>}) -> {J.lex_scan(render_after_separator(J.Arr{head <> Nil{}}, SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Punctuation{']'} <> List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)) : List<&2, J.Lexeme>}:
    Equal.trans(List<&2, J.Lexeme>,
        J.lex_scan(render_after_separator(J.Arr{head <> Nil{}}, SCon{punctuation, SNil{}} ++ suffix),
            J.Outside{}, SNil{}, acc),
        J.lex_scan(render_task(head, RenderWhole{}, "]" ++ (SCon{punctuation, SNil{}} ++ suffix)),
            J.Outside{}, SNil{}, acc),
        J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Punctuation{']'} <>
            List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)),
        Equal.cong(String, List<&2, J.Lexeme>, text => J.lex_scan(text, J.Outside{}, SNil{}, acc),
            render_after_separator(J.Arr{head <> Nil{}}, SCon{punctuation, SNil{}} ++ suffix),
            render_task(head, RenderWhole{}, "]" ++ (SCon{punctuation, SNil{}} ++ suffix)),
            render_after_separator_array_single(head, SCon{punctuation, SNil{}} ++ suffix)),
        Equal.trans(List<&2, J.Lexeme>,
            J.lex_scan(render_task(head, RenderWhole{}, "]" ++ (SCon{punctuation, SNil{}} ++ suffix)),
                J.Outside{}, SNil{}, acc),
            J.lex_scan(SCon{punctuation, SNil{}} ++ suffix, J.Outside{}, SNil{}, J.Punctuation{']'} <>
                List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)),
            J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Punctuation{']'} <>
                List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)),
            head_lex,
            W.scan_punctuation_char(punctuation, suffix, SNil{}, J.Punctuation{']'} <>
                List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc), action)))

Uses (19):
  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.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=LexAction
  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=lex_seed_action
  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_SourceProof.bend&name=RenderMode
  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_after_separator_array_single
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=render_task
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=reverse_source_task