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