the sum of the slots at a word index (there is at most one)
1012def cgSlotAt =
1013 (lambda unrestricted slots : (family StdList (family CgSlot)) .
1014 (lambda unrestricted index : Nat .
1015 (eliminate
1016 StdList
1017 (lambda unrestricted current : (family StdList (family CgSlot)) . Nat)
1018 slots
1019 (branch StdListEmpty . 0)
1020 (branch
1021 StdListCons
1022 head
1023 tail
1024 induction
1025 .
1026 (eliminate
1027 CgSlot
1028 (lambda unrestricted current : (family CgSlot) . Nat)
1029 head
1030 (branch
1031 CgSlotValue
1032 at
1033 value
1034 .
1035 (naturalAdd (naturalSelect (naturalEqual at index) value 0) 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.