def string_payload

qasim-bend-kit@0.1.0.2 · proof/JSON_StringProof.bend:1980

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

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