the block's 64-bit words, one per word a slot names (the even slot of a
pair speaks for both halves), those that are zero left out
1060def cgBlock =
1061 (lambda unrestricted slots : (family StdList (family CgSlot)) .
1062 (constructor
1063 NvidiaParameterBlock
1064 NvidiaParameterBlockValue
1065 (eliminate
1066 StdList
1067 (lambda unrestricted current : (family StdList (family CgSlot)) .
1068 (family NvidiaParameterPatches))
1069 slots
1070 (branch StdListEmpty . (constructor NvidiaParameterPatches NvidiaParameterPatchesEnd))
1071 (branch
1072 StdListCons
1073 head
1074 tail
1075 induction
1076 .
1077 (eliminate
1078 CgSlot
1079 (lambda unrestricted current : (family CgSlot) . (family NvidiaParameterPatches))
1080 head
1081 (branch
1082 CgSlotValue
1083 at
1084 value
1085 .
1086 (let unrestricted even =
1087 (naturalMultiply 2 (naturalDivideUnchecked at 2))
1088 in
1089 (let unrestricted speaks =
1090 (naturalOr (naturalEqual at even) (naturalIsZero (cgSlotPresent slots even)))
1091 in
1092 (let unrestricted word =
1093 (naturalAdd
1094 (cgSlotAt slots even)
1095 (naturalMultiply cgWordRange (cgSlotAt slots (succ even))))
1096 in
1097 (nat-eliminate
1098 (lambda unrestricted current : Nat . (family NvidiaParameterPatches))
1099 induction
1100 (lambda unrestricted q : Nat .
1101 (lambda unrestricted ignored : (family NvidiaParameterPatches) .
1102 (constructor
1103 NvidiaParameterPatches
1104 NvidiaParameterPatchesNext
1105 (constructor
1106 NvidiaParameterPatch
1107 NvidiaParameterPatchValue
1108 (naturalDivideUnchecked at 2)
1109 (modelWord64FromNaturalTruncated word))
1110 induction)))
1111 (naturalAnd speaks (naturalNonzero word))))))))))))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.