the latest ready cycle among the keys (0 when none is pending); the
comparisons are the primitive's own, eliminated where they are made
118def scReadyOf =
119 (lambda unrestricted pending : (family CompactionPending) .
120 (lambda unrestricted keys : (family StdList Nat) .
121 (eliminate StdList (lambda unrestricted current : (family StdList Nat) . Nat) keys
122 (branch StdListEmpty . zero)
123 (branch StdListCons key rest induction .
124 (scMax induction
125 (eliminate CompactionPending (lambda unrestricted current : (family CompactionPending) . Nat) pending
126 (branch CompactionPendingEnd . zero)
127 (branch CompactionPendingNext bound ready tail inner .
128 (nat-eliminate (lambda unrestricted current : Nat . Nat)
129 inner
130 (lambda unrestricted flagPredecessor : Nat . (lambda unrestricted flagRest : Nat .
131 (nat-eliminate (lambda unrestricted current : Nat . Nat)
132 ready
133 (lambda unrestricted flagPredecessor : Nat . (lambda unrestricted flagRest : Nat . inner))
134 (nat-less-than ready inner))))
135 (nat-eliminate (lambda unrestricted current : Nat . Nat)
136 (nat-eliminate (lambda unrestricted current : Nat . Nat)
137 (succ zero)
138 (lambda unrestricted flagPredecessor : Nat . (lambda unrestricted flagRest : Nat . zero))
139 (nat-less-than key bound))
140 (lambda unrestricted flagPredecessor : Nat . (lambda unrestricted flagRest : Nat . zero))
141 (nat-less-than bound key))))))))))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.