def escaped_body

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

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

1969def escaped_body(+text: String) -> {J.fast_string(J.escape_string(text) ++ "\"") == J.Decoded{text} : J.FastString}:
1970    match text:
1971        case SNil{}: {==}
1972        case SCon{h, t}:
1973            Equal.trans(J.FastString, J.fast_string((J.escape_char(h) ++ J.escape_string(t)) ++ "\""), J.fast_string(J.escape_char(h) ++ (J.escape_string(t) ++ "\"")), J.Decoded{SCon{h, t}},
1974                Equal.cong(String, J.FastString, J.fast_string, (J.escape_char(h) ++ J.escape_string(t)) ++ "\"", J.escape_char(h) ++ (J.escape_string(t) ++ "\""), append_assoc(J.escape_char(h), J.escape_string(t), "\"")),
1975                escape_one(h, J.escape_string(t) ++ "\"", t, escaped_body(t)))