`moves rest` when the subtree is reached, otherwise `rest` alone.
275def combineDeliverInto =
276 (lambda erased payload : Type 0 .
277 (lambda unrestricted reached : Nat .
278 (lambda unrestricted moves : (pi unrestricted rest : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) . (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision))) .
279 (lambda unrestricted rest : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) .
280 (nat-eliminate
281 (lambda unrestricted current : Nat .
282 (family
283 GlobalProtocol
284 (family OrderedCombineOperation payload)
285 payload
286 (family ProtocolNoDecision)))
287 rest
288 (lambda unrestricted previous : Nat .
289 (lambda unrestricted ignored : (family GlobalProtocol (family OrderedCombineOperation payload) payload (family ProtocolNoDecision)) .
290 (moves rest)))
291 reached)))))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.