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