1192def jsonObjectContainsKey =
1193 (lambda unrestricted wanted : Bytes .
1194 (lambda unrestricted members : (family JSON) .
1195 (eliminate
1196 JSON
1197 (lambda unrestricted current : (family JSON) . Nat)
1198 members
1199 (branch JSONObject nested nestedInduction . zero)
1200 (branch JSONObjectEnd . zero)
1201 (branch
1202 JSONObjectMember
1203 key
1204 value
1205 tail
1206 valueInduction
1207 tailInduction
1208 .
1209 (jsonFlagOr (bytes-equal wanted key) tailInduction))
1210 (branch JSONArray values valuesInduction . zero)
1211 (branch JSONArrayEnd . zero)
1212 (branch JSONArrayNext head tail headInduction tailInduction . zero)
1213 (branch JSONString text . zero)
1214 (branch JSONNumber number . zero)
1215 (branch JSONBoolean value . zero)
1216 (branch JSONNull . zero))))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.