1 when every element of an array is a string (1 for a chain's end)
151def aosArrayAllStrings =
152 (lambda unrestricted value : (family JSON) .
153 (eliminate
154 JSON
155 (lambda unrestricted current : (family JSON) . Nat)
156 value
157 (branch JSONObject members membersInduction . 0)
158 (branch JSONObjectEnd . 0)
159 (branch JSONObjectMember key member tail memberInduction tailInduction . 0)
160 (branch JSONArray values valuesInduction . valuesInduction)
161 (branch JSONArrayEnd . 1)
162 (branch
163 JSONArrayNext
164 head
165 tail
166 headInduction
167 tailInduction
168 .
169 (naturalAnd (aosIsString head) tailInduction))
170 (branch JSONString text . 0)
171 (branch JSONNumber digits . 0)
172 (branch JSONBoolean flag . 0)
173 (branch JSONNull . 0)))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.