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).
327def stdListNaturalEqual =
328 (lambda unrestricted expected : (family StdList Nat) .
329 (lambda unrestricted actual : (family StdList Nat) .
330 (app
331 (eliminate
332 StdList
333 (lambda unrestricted current : (family StdList Nat) .
334 (pi unrestricted other : (family StdList Nat) . (family StdBool)))
335 expected
336 (branch
337 StdListEmpty
338 .
339 (lambda unrestricted other : (family StdList Nat) . (stdListIsEmpty Nat other)))
340 (branch
341 StdListCons
342 head
343 tail
344 induction
345 .
346 (lambda unrestricted other : (family StdList Nat) .
347 (eliminate
348 StdList
349 (lambda unrestricted current : (family StdList Nat) . (family StdBool))
350 other
351 (branch StdListEmpty . (constructor StdBool StdFalse))
352 (branch
353 StdListCons
354 otherHead
355 otherTail
356 otherInduction
357 .
358 (stdBoolAnd
359 (stdOrderIsEqual (stdOrderCompareNatural head otherHead))
360 (induction otherTail)))))))
361 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.