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