1034def livenessReplaceSlot =
1035 (lambda unrestricted oldSlot : (family LivenessSlot) .
1036 (lambda unrestricted newSlot : (family LivenessSlot) .
1037 (lambda unrestricted slots : (family LivenessSlots) .
1038 (eliminate
1039 LivenessSlot
1040 (lambda unrestricted current : (family LivenessSlot) . (family LivenessSlots))
1041 oldSlot
1042 (branch
1043 LivenessSlotValue
1044 oldOffset
1045 oldCapacity
1046 oldLastUse
1047 .
1048 (eliminate
1049 LivenessSlots
1050 (lambda unrestricted current : (family LivenessSlots) . (family LivenessSlots))
1051 slots
1052 (branch LivenessSlotsEnd . (constructor LivenessSlots LivenessSlotsEnd))
1053 (branch
1054 LivenessSlotsNext
1055 head
1056 tail
1057 ih_tail
1058 .
1059 (eliminate
1060 LivenessSlot
1061 (lambda unrestricted current : (family LivenessSlot) . (family LivenessSlots))
1062 head
1063 (branch
1064 LivenessSlotValue
1065 offset
1066 capacity
1067 lastUse
1068 .
1069 (nat-eliminate
1070 (lambda unrestricted sameOffset : Nat . (family LivenessSlots))
1071 (constructor LivenessSlots LivenessSlotsNext head ih_tail)
1072 (lambda unrestricted predecessor : Nat .
1073 (lambda unrestricted induction : (family LivenessSlots) .
1074 (constructor LivenessSlots LivenessSlotsNext newSlot tail)))
1075 (modelWord64Equal (stdByteCountValue offset) (stdByteCountValue oldOffset))))))))))))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.