ranges in reverse order of addition; a range that starts where the
last one ends extends it
2733def cgPush =
2734 (lambda unrestricted ranges : (family StdList (family CgRange)) .
2735 (lambda unrestricted first : Nat .
2736 (lambda unrestricted count : Nat .
2737 (eliminate
2738 StdList
2739 (lambda unrestricted current : (family StdList (family CgRange)) .
2740 (family StdList (family CgRange)))
2741 ranges
2742 (branch
2743 StdListEmpty
2744 .
2745 (constructor
2746 StdList
2747 StdListCons
2748 (family CgRange)
2749 (constructor CgRange CgRangeValue first count)
2750 ranges))
2751 (branch
2752 StdListCons
2753 head
2754 tail
2755 induction
2756 .
2757 (eliminate
2758 CgRange
2759 (lambda unrestricted current : (family CgRange) . (family StdList (family CgRange)))
2760 head
2761 (branch
2762 CgRangeValue
2763 lastFirst
2764 lastCount
2765 .
2766 (nat-eliminate
2767 (lambda unrestricted current : Nat . (family StdList (family CgRange)))
2768 (constructor
2769 StdList
2770 StdListCons
2771 (family CgRange)
2772 (constructor CgRange CgRangeValue first count)
2773 ranges)
2774 (lambda unrestricted q : Nat .
2775 (lambda unrestricted ignored : (family StdList (family CgRange)) .
2776 (constructor
2777 StdList
2778 StdListCons
2779 (family CgRange)
2780 (constructor CgRange CgRangeValue lastFirst (naturalAdd lastCount count))
2781 tail)))
2782 (naturalEqual (naturalAdd lastFirst lastCount) first)))))))))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.