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