JSONLexWhitespaceProof.scan_escape_string: 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 297-315 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=297&end_line=315

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_StringProof.bend as S

def scan_escape_string(+text: String,
                       +suffix: String,
                       +reversed: String,
                       +acc: List<&2, J.Lexeme>) -> {J.lex_scan(J.escape_string(text) ++ suffix, J.Quoted{}, reversed, acc) == J.lex_scan(suffix, J.Quoted{}, escape_reverse(text, reversed), acc) : List<&2, J.Lexeme>}:
    match text:
        case SNil{}: {==}
        case SCon{+head, +tail}:
            Equal.trans(List<&2, J.Lexeme>, J.lex_scan(J.escape_string(text) ++ suffix, J.Quoted{}, reversed, acc),
                J.lex_scan(J.escape_char(head) ++ (J.escape_string(tail) ++ suffix), J.Quoted{}, reversed, acc),
                J.lex_scan(suffix, J.Quoted{}, escape_reverse(text, reversed), acc),
                Equal.cong(String, List<&2, J.Lexeme>, source => J.lex_scan(source, J.Quoted{}, reversed, acc),
                    J.escape_string(text) ++ suffix, J.escape_char(head) ++ (J.escape_string(tail) ++ suffix),
                    S.append_assoc(J.escape_char(head), J.escape_string(tail), suffix)),
                Equal.trans(List<&2, J.Lexeme>,
                    J.lex_scan(J.escape_char(head) ++ (J.escape_string(tail) ++ suffix), J.Quoted{}, reversed, acc),
                    J.lex_scan(J.escape_string(tail) ++ suffix, J.Quoted{}, String.reverse(J.escape_char(head)) ++ reversed, acc),
                    J.lex_scan(suffix, J.Quoted{}, escape_reverse(text, reversed), acc),
                    scan_escape_char(head, J.escape_string(tail) ++ suffix, reversed, acc, J.escape_class(head), {==}),
                    scan_escape_string(tail, suffix, String.reverse(J.escape_char(head)) ++ reversed, acc)))

Uses (15):
  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=Base/base.bend&name=String.append
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String.reverse
  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=escape_char
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=escape_class
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=escape_string
  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/proof/JSON_LexWhitespaceProof.bend&name=escape_reverse
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_LexWhitespaceProof.bend&name=scan_escape_char
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_StringProof.bend&name=append_assoc