JSONLexWhitespaceProof.scan_punctuation_char: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/JSON_LexWhitespaceProof.bend as JSONLexWhitespaceProof
Lines 166-187 of qasim-bend-kit@0.1.0.2/proof/JSON_LexWhitespaceProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_LexWhitespaceProof.bend&start_line=166&end_line=187

import Base
import qasim-bend-kit@0.1.0.2/libs/JSON.bend as J

def scan_punctuation_char(+character: Char,
                          +tail: String,
                          +reversed: String,
                          +acc: List<&2, J.Lexeme>,
                          action: {J.lex_seed_action(SCon{character, tail}, J.Outside{}) == J.LexPunctuation{character} : J.LexAction}) -> {J.lex_scan(SCon{character, tail}, J.Outside{}, reversed, acc) == J.lex_scan(tail, J.Outside{}, SNil{}, J.Punctuation{character} <> J.flush_lexeme(reversed, acc)) : List<&2, J.Lexeme>}:
    Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{character, tail}, J.Outside{}, reversed, acc),
        J.lex_scan(tail, after_mode(J.LexPunctuation{character}, J.Outside{}),
            after_reversed(J.LexPunctuation{character}, character, reversed),
            after_acc(J.LexPunctuation{character}, character, reversed, acc)),
        J.lex_scan(tail, J.Outside{}, SNil{}, J.Punctuation{character} <> J.flush_lexeme(reversed, acc)),
        Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{character, tail}, J.Outside{}, reversed, acc),
            J.lex_scan(tail, after_mode(J.lex_seed_action(SCon{character, tail}, J.Outside{}), J.Outside{}),
                after_reversed(J.lex_seed_action(SCon{character, tail}, J.Outside{}), character, reversed),
                after_acc(J.lex_seed_action(SCon{character, tail}, J.Outside{}), character, reversed, acc)),
            J.lex_scan(tail, after_mode(J.LexPunctuation{character}, J.Outside{}),
                after_reversed(J.LexPunctuation{character}, character, reversed),
                after_acc(J.LexPunctuation{character}, character, reversed, acc)),
            lex_scan_step(character, tail, J.Outside{}, reversed, acc),
            Equal.cong(J.LexAction, List<&2, J.Lexeme>, action => J.lex_scan(tail, after_mode(action, J.Outside{}),
                after_reversed(action, character, reversed), after_acc(action, character, reversed, acc)),
                J.lex_seed_action(SCon{character, tail}, J.Outside{}), J.LexPunctuation{character}, action)),
        {==})

Uses (15):
  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=String
  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=flush_lexeme
  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=after_acc
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_LexWhitespaceProof.bend&name=after_mode
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_LexWhitespaceProof.bend&name=after_reversed
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_LexWhitespaceProof.bend&name=lex_scan_step