Data.JSONAccess

287def jsonObject =
288  (lambda unrestricted value : (family JSON) .
289    (eliminate
290      JSON
291      (lambda unrestricted current : (family JSON) . (family JSONObjectAccessResult))
292      value
293      (branch
294        JSONObject
295        members
296        membersInduction
297        .
298        (eliminate
299          JSONTreeAuditResult
300          (lambda unrestricted current : (family JSONTreeAuditResult) .
301            (family JSONObjectAccessResult))
302          (jsonAuditTreeWithTokenLimits
303            (constructor JSONBound JSONBoundBelowTwoPower jsonNaturalTwenty)
304            (constructor JSONBound JSONBoundAtMost jsonNaturalOneThousandTwentyFour)
305            (constructor JSONBound JSONBoundAtMost jsonNaturalSixtyFiveThousandFiveHundredThirtySix)
306            value)
307          (branch
308            JSONTreeAuditSucceeded
309            kind
310            counts
311            depth
312            sequenceCount
313            .
314            (constructor JSONObjectAccessResult JSONObjectAccessSucceeded members))
315          (branch
316            JSONTreeAuditFailed
317            code
318            .
319            (constructor JSONObjectAccessResult JSONObjectAccessFailed code))))
320      (branch
321        JSONObjectEnd
322        .
323        (constructor
324          JSONObjectAccessResult
325          JSONObjectAccessFailed
326          (constructor JSONErrorCode JSONExpectedObject)))
327      (branch
328        JSONObjectMember
329        key
330        member
331        tail
332        memberInduction
333        tailInduction
334        .
335        (constructor
336          JSONObjectAccessResult
337          JSONObjectAccessFailed
338          (constructor JSONErrorCode JSONExpectedObject)))
339      (branch
340        JSONArray
341        values
342        valuesInduction
343        .
344        (constructor
345          JSONObjectAccessResult
346          JSONObjectAccessFailed
347          (constructor JSONErrorCode JSONExpectedObject)))
348      (branch
349        JSONArrayEnd
350        .
351        (constructor
352          JSONObjectAccessResult
353          JSONObjectAccessFailed
354          (constructor JSONErrorCode JSONExpectedObject)))
355      (branch
356        JSONArrayNext
357        head
358        tail
359        headInduction
360        tailInduction
361        .
362        (constructor
363          JSONObjectAccessResult
364          JSONObjectAccessFailed
365          (constructor JSONErrorCode JSONExpectedObject)))
366      (branch
367        JSONString
368        text
369        .
370        (constructor
371          JSONObjectAccessResult
372          JSONObjectAccessFailed
373          (constructor JSONErrorCode JSONExpectedObject)))
374      (branch
375        JSONNumber
376        number
377        .
378        (constructor
379          JSONObjectAccessResult
380          JSONObjectAccessFailed
381          (constructor JSONErrorCode JSONExpectedObject)))
382      (branch
383        JSONBoolean
384        boolean
385        .
386        (constructor
387          JSONObjectAccessResult
388          JSONObjectAccessFailed
389          (constructor JSONErrorCode JSONExpectedObject)))
390      (branch
391        JSONNull
392        .
393        (constructor
394          JSONObjectAccessResult
395          JSONObjectAccessFailed
396          (constructor JSONErrorCode JSONExpectedObject)))))