whether a slot sits at a word index
1039def cgSlotPresent =
1040 (lambda unrestricted slots : (family StdList (family CgSlot)) .
1041 (lambda unrestricted index : Nat .
1042 (eliminate
1043 StdList
1044 (lambda unrestricted current : (family StdList (family CgSlot)) . Nat)
1045 slots
1046 (branch StdListEmpty . 0)
1047 (branch
1048 StdListCons
1049 head
1050 tail
1051 induction
1052 .
1053 (eliminate
1054 CgSlot
1055 (lambda unrestricted current : (family CgSlot) . Nat)
1056 head
1057 (branch CgSlotValue at value . (naturalOr (naturalEqual at index) induction)))))))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.