def nested_render_append

qasim-bend-kit@0.1.0.2 · proof/JSON_SourceProof.bend:32

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

32def nested_render_append(+outer: J.Value,
33                         +inner: J.Value,
34                         +inner_members: Bool,
35                         +prefix: String,
36                         +suffix: String,
37                         +outer_append: {J.render(outer, False{}, J.render(inner, inner_members, prefix)) ++ suffix == J.render(outer, False{}, J.render(inner, inner_members, prefix) ++ suffix) : String},
38                         +inner_append: {J.render(inner, inner_members, prefix) ++ suffix == J.render(inner, inner_members, prefix ++ suffix) : String}) -> {J.render(outer, False{}, J.render(inner, inner_members, prefix)) ++ suffix == J.render(outer, False{}, J.render(inner, inner_members, prefix ++ suffix)) : String}:
39    Equal.trans(String,
40        J.render(outer, False{}, J.render(inner, inner_members, prefix)) ++ suffix,
41        J.render(outer, False{}, J.render(inner, inner_members, prefix) ++ suffix),
42        J.render(outer, False{}, J.render(inner, inner_members, prefix ++ suffix)),
43        outer_append,
44        Equal.cong(String, String, text => J.render(outer, False{}, text),
45            J.render(inner, inner_members, prefix) ++ suffix,
46            J.render(inner, inner_members, prefix ++ suffix),
47            inner_append))