---------------------------------------------------------------------------
The verdict
724def aosSumGaps =
725 (lambda unrestricted producers : (family StdList (family AosProducer)) .
726 (lambda unrestricted withDrops : Nat .
727 (eliminate
728 StdList
729 (lambda unrestricted current : (family StdList (family AosProducer)) . Nat)
730 producers
731 (branch StdListEmpty . 0)
732 (branch
733 StdListCons
734 head
735 tail
736 induction
737 .
738 (naturalAdd
739 induction
740 (eliminate
741 AosProducer
742 (lambda unrestricted current : (family AosProducer) . Nat)
743 head
744 (branch
745 AosProducerValue
746 key
747 next
748 seen
749 drops
750 covered
751 excluded
752 mode
753 .
754 (naturalSaturatingSubtract
755 (naturalSaturatingSubtract
756 (aosChoose Nat (naturalLess next covered) covered next)
757 seen)
758 (naturalSelect withDrops drops 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.