Structural equality of two lists of naturals: same length, same elements in
the same order. The first list is eliminated into a FUNCTION of the second,
so the recursion walks both spines together. A proof about two computed
lists states this closed verdict rather than an equation between them: an
equation between two lists built by the same builder is compared
symbolically first (the builders' element functions, under a binder),
which costs far more than computing them (Proof.CheckedHMMATile's instance
words: 580 s against 34 s).
272def stdListNaturalEqual =
273 (lambda unrestricted expected : (family StdList Nat) .
274 (lambda unrestricted actual : (family StdList Nat) .
275 (app
276 (eliminate
277 StdList
278 (lambda unrestricted current : (family StdList Nat) .
279 (pi unrestricted other : (family StdList Nat) . (family StdBool)))
280 expected
281 (branch
282 StdListEmpty
283 .
284 (lambda unrestricted other : (family StdList Nat) . (stdListIsEmpty Nat other)))
285 (branch
286 StdListCons
287 head
288 tail
289 induction
290 .
291 (lambda unrestricted other : (family StdList Nat) .
292 (eliminate
293 StdList
294 (lambda unrestricted current : (family StdList Nat) . (family StdBool))
295 other
296 (branch StdListEmpty . (constructor StdBool StdFalse))
297 (branch
298 StdListCons
299 otherHead
300 otherTail
301 otherInduction
302 .
303 (stdBoolAnd
304 (stdOrderIsEqual (stdOrderCompareNatural head otherHead))
305 (induction otherTail)))))))
306 actual)))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.