JSONStringProof.string_payload: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/JSON_StringProof.bend as JSONStringProof
Lines 1980-1984 of qasim-bend-kit@0.1.0.2/proof/JSON_StringProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_StringProof.bend&start_line=1980&end_line=1984

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_PrimitiveProof.bend as P

def string_payload(+text: String) -> {J.decode_payload("\"" ++ J.escape_string(text) ++ "\"") == Done{J.Str{text}} : Result<&1, &1, J.Error, J.Value>}:
    Equal.trans(P.R(), J.decode_payload("\"" ++ J.escape_string(text) ++ "\""), J.payload_other("\"" ++ J.escape_string(text) ++ "\""), Done{J.Str{text}},
        P.decode_false("\"" ++ J.escape_string(text) ++ "\"", number_quote(J.escape_string(text) ++ "\"")),
        Equal.cong(J.FastString, P.R(), r => J.fast_result(r, "\"" ++ J.escape_string(text) ++ "\""),
            J.fast_string(J.escape_string(text) ++ "\""), J.Decoded{text}, escaped_body(text)))

Uses (17):
  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=Result
  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=Error
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=FastString
  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=decode_payload
  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=fast_result
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=fast_string
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=payload_other
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_PrimitiveProof.bend&name=R
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_PrimitiveProof.bend&name=decode_false
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_StringProof.bend&name=escaped_body
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_StringProof.bend&name=number_quote