def field_text

qasim-bend-kit@0.1.0.2 · proof/JSON_RenderLexProof.bend:309

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

309def field_text(+key: String,
310               +text: String) -> {J.render_object_field(SNil{}, key, text) == ("\"" ++ J.escape_string(key) ++ "\"") ++ (":" ++ text) : String}:
311    Equal.trans(String,
312        J.render_object_field(SNil{}, key, text),
313        SCon{'"', J.escape_string(key) ++ ("\":" ++ text)},
314        ("\"" ++ J.escape_string(key) ++ "\"") ++ (":" ++ text),
315        Equal.cong(String, String,
316            x => SCon{'"', x},
317            (J.escape_string(key) ++ "\":") ++ text,
318            J.escape_string(key) ++ ("\":" ++ text),
319            S.append_assoc(J.escape_string(key), "\":", text)),
320        Equal.sym(String,
321            ("\"" ++ J.escape_string(key) ++ "\"") ++ (":" ++ text),
322            SCon{'"', J.escape_string(key) ++ ("\":" ++ text)},
323            Equal.cong(String, String,
324                x => SCon{'"', x},
325                (J.escape_string(key) ++ "\"") ++ (":" ++ text),
326                J.escape_string(key) ++ ("\"" ++ (":" ++ text)),
327                S.append_assoc(J.escape_string(key), "\"", ":" ++ text))))