JSONLexWhitespaceProof.lex_rendered_string_suffix: 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 353-388 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=353&end_line=388

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 lex_rendered_string_suffix(+text: String,
                               +suffix: String,
                               +acc: List<&2, J.Lexeme>) -> {J.lex_scan((SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}) ++ suffix, J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Payload{SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}} <> acc) : List<&2, J.Lexeme>}:
    Equal.trans(List<&2, J.Lexeme>,
        J.lex_scan((SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}) ++ suffix, J.Outside{}, SNil{}, acc),
        J.lex_scan(SCon{'"', (J.escape_string(text) ++ SCon{'"', SNil{}}) ++ suffix}, J.Outside{}, SNil{}, acc),
        J.lex_scan(suffix, J.Outside{}, SNil{}, J.Payload{SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}} <> acc),
        Equal.cong(String, List<&2, J.Lexeme>, source => J.lex_scan(source, J.Outside{}, SNil{}, acc),
            (SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}) ++ suffix,
            SCon{'"', (J.escape_string(text) ++ SCon{'"', SNil{}}) ++ suffix}, {==}),
        Equal.trans(List<&2, J.Lexeme>,
            J.lex_scan(SCon{'"', (J.escape_string(text) ++ SCon{'"', SNil{}}) ++ suffix}, J.Outside{}, SNil{}, acc),
            J.lex_scan((J.escape_string(text) ++ SCon{'"', SNil{}}) ++ suffix, J.Quoted{}, SCon{'"', SNil{}}, acc),
            J.lex_scan(suffix, J.Outside{}, SNil{}, J.Payload{SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}} <> acc),
            lex_scan_step('"', (J.escape_string(text) ++ SCon{'"', SNil{}}) ++ suffix, J.Outside{}, SNil{}, acc),
            Equal.trans(List<&2, J.Lexeme>,
                J.lex_scan((J.escape_string(text) ++ SCon{'"', SNil{}}) ++ suffix, J.Quoted{}, SCon{'"', SNil{}}, acc),
                J.lex_scan(J.escape_string(text) ++ (SCon{'"', SNil{}} ++ suffix), J.Quoted{}, SCon{'"', SNil{}}, acc),
                J.lex_scan(suffix, J.Outside{}, SNil{}, J.Payload{SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}} <> acc),
                Equal.cong(String, List<&2, J.Lexeme>, source => J.lex_scan(source, J.Quoted{}, SCon{'"', SNil{}}, acc),
                    (J.escape_string(text) ++ SCon{'"', SNil{}}) ++ suffix,
                    J.escape_string(text) ++ (SCon{'"', SNil{}} ++ suffix),
                    S.append_assoc(J.escape_string(text), SCon{'"', SNil{}}, suffix)),
                Equal.trans(List<&2, J.Lexeme>,
                    J.lex_scan(J.escape_string(text) ++ (SCon{'"', SNil{}} ++ suffix), J.Quoted{}, SCon{'"', SNil{}}, acc),
                    J.lex_scan(SCon{'"', SNil{}} ++ suffix, J.Quoted{}, escape_reverse(text, SCon{'"', SNil{}}), acc),
                    J.lex_scan(suffix, J.Outside{}, SNil{}, J.Payload{SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}} <> acc),
                    scan_escape_string(text, SCon{'"', SNil{}} ++ suffix, SCon{'"', SNil{}}, acc),
                    Equal.trans(List<&2, J.Lexeme>,
                        J.lex_scan(SCon{'"', SNil{}} ++ suffix, J.Quoted{}, escape_reverse(text, SCon{'"', SNil{}}), acc),
                        J.lex_scan(suffix, J.Outside{}, SNil{}, J.Payload{String.reverse(SCon{'"', escape_reverse(text, SCon{'"', SNil{}})})} <> acc),
                        J.lex_scan(suffix, J.Outside{}, SNil{}, J.Payload{SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}} <> acc),
                        lex_scan_step('"', suffix, J.Quoted{}, escape_reverse(text, SCon{'"', SNil{}}), acc),
                        Equal.cong(String, List<&2, J.Lexeme>, payload => J.lex_scan(suffix, J.Outside{}, SNil{}, J.Payload{payload} <> acc),
                            String.reverse(SCon{'"', escape_reverse(text, SCon{'"', SNil{}})}),
                            SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}, quoted_buffer_payload(text)))))))

Uses (16):
  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=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_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=lex_scan_step
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_LexWhitespaceProof.bend&name=quoted_buffer_payload
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_LexWhitespaceProof.bend&name=scan_escape_string
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_StringProof.bend&name=append_assoc