Part of `jsonRenderTree`, lifted out to keep it inside the §28.3 size and
nesting limits; the parameters are the locals it still needs.
204def jsonRenderTreePart1 =
205 (lambda unrestricted key : Bytes .
206 (lambda unrestricted memberInduction : (family JSONRenderFragment) .
207 (lambda unrestricted tailInduction : (family JSONRenderFragment) .
208 (eliminate
209 JSONRenderFragment
210 (lambda unrestricted current : (family JSONRenderFragment) . (family JSONRenderFragment))
211 (jsonRenderStringFragment key)
212 (branch
213 JSONRenderFragmentSucceeded
214 keyKind
215 keyBuilder
216 keyCount
217 .
218 (eliminate
219 JSONRenderFragment
220 (lambda unrestricted current : (family JSONRenderFragment) .
221 (family JSONRenderFragment))
222 memberInduction
223 (branch
224 JSONRenderFragmentSucceeded
225 memberKind
226 memberBuilder
227 memberCount
228 .
229 (eliminate
230 JSONRenderFragment
231 (lambda unrestricted current : (family JSONRenderFragment) .
232 (family JSONRenderFragment))
233 tailInduction
234 (branch
235 JSONRenderFragmentSucceeded
236 tailKind
237 tailBuilder
238 tailCount
239 .
240 (nat-eliminate
241 (lambda unrestricted validKey : Nat . (family JSONRenderFragment))
242 jsonRenderFailure
243 (lambda unrestricted keyPredecessor : Nat .
244 (lambda unrestricted keyInduction : (family JSONRenderFragment) .
245 (nat-eliminate
246 (lambda unrestricted validMember : Nat . (family JSONRenderFragment))
247 jsonRenderFailure
248 (lambda unrestricted memberPredecessor : Nat .
249 (lambda unrestricted memberRoleInduction : (family JSONRenderFragment) .
250 (nat-eliminate
251 (lambda unrestricted validTail : Nat .
252 (family JSONRenderFragment))
253 jsonRenderFailure
254 (lambda unrestricted tailPredecessor : Nat .
255 (lambda unrestricted tailRoleInduction : (family JSONRenderFragment) .
256 (constructor
257 JSONRenderFragment
258 JSONRenderFragmentSucceeded
259 (constructor JSONRenderKind JSONRenderObjectMembersKind)
260 (bytes-builder-append
261 keyBuilder
262 (bytes-builder-append
263 (bytes-builder-chunk b":")
264 (bytes-builder-append
265 memberBuilder
266 (bytes-builder-append
267 (jsonRenderCommaBefore tailCount)
268 tailBuilder))))
269 (succ tailCount))))
270 (jsonRenderKindIsObjectMembers tailKind))))
271 (jsonRenderKindIsValue memberKind))))
272 (jsonRenderKindIsValue keyKind)))
273 (branch
274 JSONRenderFragmentFailed
275 code
276 .
277 (constructor JSONRenderFragment JSONRenderFragmentFailed code))))
278 (branch
279 JSONRenderFragmentFailed
280 code
281 .
282 (constructor JSONRenderFragment JSONRenderFragmentFailed code))))
283 (branch
284 JSONRenderFragmentFailed
285 code
286 .
287 (constructor JSONRenderFragment JSONRenderFragmentFailed code))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.