JSONLexWhitespaceProof.lex_rendered_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 333-351 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=333&end_line=351

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

def lex_rendered_string(+text: String) -> {J.lex_scan(SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}, J.Outside{}, SNil{}, Nil{}) == J.Payload{SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}} <> Nil{} : List<&2, J.Lexeme>}:
    Equal.trans(List<&2, J.Lexeme>,
        J.lex_scan(SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}, J.Outside{}, SNil{}, Nil{}),
        J.lex_scan(J.escape_string(text) ++ SCon{'"', SNil{}}, J.Quoted{}, SCon{'"', SNil{}}, Nil{}),
        J.Payload{SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}} <> Nil{},
        lex_scan_step('"', J.escape_string(text) ++ SCon{'"', SNil{}}, J.Outside{}, SNil{}, Nil{}),
        Equal.trans(List<&2, J.Lexeme>,
            J.lex_scan(J.escape_string(text) ++ SCon{'"', SNil{}}, J.Quoted{}, SCon{'"', SNil{}}, Nil{}),
            J.lex_scan(SCon{'"', SNil{}}, J.Quoted{}, escape_reverse(text, SCon{'"', SNil{}}), Nil{}),
            J.Payload{SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}} <> Nil{},
            scan_escape_string(text, SCon{'"', SNil{}}, SCon{'"', SNil{}}, Nil{}),
            Equal.trans(List<&2, J.Lexeme>,
                J.lex_scan(SCon{'"', SNil{}}, J.Quoted{}, escape_reverse(text, SCon{'"', SNil{}}), Nil{}),
                J.Payload{String.reverse(SCon{'"', escape_reverse(text, SCon{'"', SNil{}})})} <> Nil{},
                J.Payload{SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}} <> Nil{},
                lex_scan_step('"', SNil{}, J.Quoted{}, escape_reverse(text, SCon{'"', SNil{}}), Nil{}),
                Equal.cong(String, List<&2, J.Lexeme>, payload => J.Payload{payload} <> Nil{},
                    String.reverse(SCon{'"', escape_reverse(text, SCon{'"', SNil{}})}),
                    SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}, quoted_buffer_payload(text)))))

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=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