Data.JSONAccess

505def jsonArray =
506  (lambda unrestricted value : (family JSON) .
507    (eliminate
508      JSON
509      (lambda unrestricted current : (family JSON) . (family JSONArrayAccessResult))
510      value
511      (branch
512        JSONObject
513        members
514        membersInduction
515        .
516        (constructor
517          JSONArrayAccessResult
518          JSONArrayAccessFailed
519          (constructor JSONErrorCode JSONExpectedArray)))
520      (branch
521        JSONObjectEnd
522        .
523        (constructor
524          JSONArrayAccessResult
525          JSONArrayAccessFailed
526          (constructor JSONErrorCode JSONExpectedArray)))
527      (branch
528        JSONObjectMember
529        key
530        member
531        tail
532        memberInduction
533        tailInduction
534        .
535        (constructor
536          JSONArrayAccessResult
537          JSONArrayAccessFailed
538          (constructor JSONErrorCode JSONExpectedArray)))
539      (branch
540        JSONArray
541        values
542        valuesInduction
543        .
544        (constructor JSONArrayAccessResult JSONArrayAccessSucceeded values))
545      (branch
546        JSONArrayEnd
547        .
548        (constructor
549          JSONArrayAccessResult
550          JSONArrayAccessFailed
551          (constructor JSONErrorCode JSONExpectedArray)))
552      (branch
553        JSONArrayNext
554        head
555        tail
556        headInduction
557        tailInduction
558        .
559        (constructor
560          JSONArrayAccessResult
561          JSONArrayAccessFailed
562          (constructor JSONErrorCode JSONExpectedArray)))
563      (branch
564        JSONString
565        text
566        .
567        (constructor
568          JSONArrayAccessResult
569          JSONArrayAccessFailed
570          (constructor JSONErrorCode JSONExpectedArray)))
571      (branch
572        JSONNumber
573        number
574        .
575        (constructor
576          JSONArrayAccessResult
577          JSONArrayAccessFailed
578          (constructor JSONErrorCode JSONExpectedArray)))
579      (branch
580        JSONBoolean
581        boolean
582        .
583        (constructor
584          JSONArrayAccessResult
585          JSONArrayAccessFailed
586          (constructor JSONErrorCode JSONExpectedArray)))
587      (branch
588        JSONNull
589        .
590        (constructor
591          JSONArrayAccessResult
592          JSONArrayAccessFailed
593          (constructor JSONErrorCode JSONExpectedArray)))))