Data.JSONAccess

96def jsonLookupMembers =
97  (lambda unrestricted wanted : Bytes .
98    (lambda unrestricted members : (family JSON) .
99      (eliminate
100        JSON
101        (lambda unrestricted current : (family JSON) . (family JSONMemberLookupResult))
102        members
103        (branch
104          JSONObject
105          nested
106          nestedInduction
107          .
108          (constructor JSONMemberLookupResult JSONMemberTreeMalformed))
109        (branch JSONObjectEnd . (constructor JSONMemberLookupResult JSONMemberMissing))
110        (branch
111          JSONObjectMember
112          key
113          value
114          tail
115          valueInduction
116          tailInduction
117          .
118          (nat-eliminate
119            (lambda unrestricted matches : Nat . (family JSONMemberLookupResult))
120            tailInduction
121            (lambda unrestricted predecessor : Nat .
122              (lambda unrestricted induction : (family JSONMemberLookupResult) .
123                (eliminate
124                  JSONMemberLookupResult
125                  (lambda unrestricted current : (family JSONMemberLookupResult) .
126                    (family JSONMemberLookupResult))
127                  tailInduction
128                  (branch
129                    JSONMemberMissing
130                    .
131                    (constructor JSONMemberLookupResult JSONMemberFound value))
132                  (branch
133                    JSONMemberFound
134                    duplicateValue
135                    .
136                    (constructor JSONMemberLookupResult JSONMemberDuplicated))
137                  (branch
138                    JSONMemberDuplicated
139                    .
140                    (constructor JSONMemberLookupResult JSONMemberDuplicated))
141                  (branch
142                    JSONMemberTreeMalformed
143                    .
144                    (constructor JSONMemberLookupResult JSONMemberTreeMalformed)))))
145            (bytes-equal wanted key)))
146        (branch
147          JSONArray
148          values
149          valuesInduction
150          .
151          (constructor JSONMemberLookupResult JSONMemberTreeMalformed))
152        (branch JSONArrayEnd . (constructor JSONMemberLookupResult JSONMemberTreeMalformed))
153        (branch
154          JSONArrayNext
155          head
156          tail
157          headInduction
158          tailInduction
159          .
160          (constructor JSONMemberLookupResult JSONMemberTreeMalformed))
161        (branch JSONString text . (constructor JSONMemberLookupResult JSONMemberTreeMalformed))
162        (branch JSONNumber number . (constructor JSONMemberLookupResult JSONMemberTreeMalformed))
163        (branch JSONBoolean value . (constructor JSONMemberLookupResult JSONMemberTreeMalformed))
164        (branch JSONNull . (constructor JSONMemberLookupResult JSONMemberTreeMalformed)))))