996def livenessBestReusable =
997 (lambda unrestricted lifetime : (family Lifetime) .
998 (lambda unrestricted slots : (family LivenessSlots) .
999 (eliminate
1000 LivenessSlots
1001 (lambda unrestricted current : (family LivenessSlots) . (family LivenessOptionalSlot))
1002 slots
1003 (branch LivenessSlotsEnd . (constructor LivenessOptionalSlot LivenessNoSlot))
1004 (branch
1005 LivenessSlotsNext
1006 head
1007 tail
1008 ih_tail
1009 .
1010 (nat-eliminate
1011 (lambda unrestricted reusable : Nat . (family LivenessOptionalSlot))
1012 ih_tail
1013 (lambda unrestricted predecessor : Nat .
1014 (lambda unrestricted induction : (family LivenessOptionalSlot) .
1015 (eliminate
1016 LivenessOptionalSlot
1017 (lambda unrestricted current : (family LivenessOptionalSlot) .
1018 (family LivenessOptionalSlot))
1019 ih_tail
1020 (branch LivenessNoSlot . (constructor LivenessOptionalSlot LivenessSomeSlot head))
1021 (branch
1022 LivenessSomeSlot
1023 selected
1024 .
1025 (nat-eliminate
1026 (lambda unrestricted better : Nat . (family LivenessOptionalSlot))
1027 ih_tail
1028 (lambda unrestricted betterPredecessor : Nat .
1029 (lambda unrestricted ignored : (family LivenessOptionalSlot) .
1030 (constructor LivenessOptionalSlot LivenessSomeSlot head)))
1031 (livenessSlotBetter head selected))))))
1032 (livenessSlotReusable lifetime head))))))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.