the adjustments naming a launch (by one of its ordinals, or all blocks)
folded into its spans by `step`
924def deviceArenaFold =
925 (lambda unrestricted step : (pi unrestricted ordinal : Nat . (pi unrestricted offset : Nat . (pi unrestricted value : Nat . (pi unrestricted spans : (family DeviceArenaSpans) . (family DeviceArenaSpans))))) .
926 (lambda unrestricted adjustments : (family NvidiaParameterAdjustments) .
927 (lambda unrestricted launch : (family DeviceArenaLaunch) .
928 (eliminate
929 DeviceArenaLaunch
930 (lambda unrestricted current : (family DeviceArenaLaunch) . (family DeviceArenaLaunch))
931 launch
932 (branch
933 DeviceArenaLaunchValue
934 identity
935 base
936 generators
937 spans
938 .
939 (constructor
940 DeviceArenaLaunch
941 DeviceArenaLaunchValue
942 identity
943 base
944 generators
945 (eliminate
946 NvidiaParameterAdjustments
947 (lambda unrestricted current : (family NvidiaParameterAdjustments) .
948 (family DeviceArenaSpans))
949 adjustments
950 (branch NvidiaParameterAdjustmentsEnd . spans)
951 (branch
952 NvidiaParameterAdjustmentsNext
953 head
954 tail
955 induction
956 .
957 (eliminate
958 NvidiaParameterAdjustment
959 (lambda unrestricted current : (family NvidiaParameterAdjustment) .
960 (family DeviceArenaSpans))
961 head
962 (branch
963 NvidiaParameterAdjustmentValue
964 scope
965 offset
966 value
967 .
968 (nat-eliminate
969 (lambda unrestricted applies : Nat . (family DeviceArenaSpans))
970 induction
971 (lambda unrestricted q : Nat .
972 (lambda unrestricted ignored : (family DeviceArenaSpans) .
973 (step
974 (eliminate
975 NvidiaParameterAdjustmentScope
976 (lambda unrestricted current : (family NvidiaParameterAdjustmentScope) .
977 Nat)
978 scope
979 (branch NvidiaParameterAdjustmentAllBlocks . deviceArenaWordMaximum)
980 (branch NvidiaParameterAdjustmentBlock at . at))
981 offset
982 (modelWord64Natural value)
983 induction)))
984 (eliminate
985 NvidiaParameterAdjustmentScope
986 (lambda unrestricted current : (family NvidiaParameterAdjustmentScope) .
987 Nat)
988 scope
989 (branch NvidiaParameterAdjustmentAllBlocks . 1)
990 (branch
991 NvidiaParameterAdjustmentBlock
992 at
993 .
994 (deviceArenaGenerated base generators at))))))))))))))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.