2840def cgSubmissionFor =
2841 (lambda unrestricted count : Nat .
2842 (lambda unrestricted body : (pi unrestricted index : Nat . (family NvidiaSubmissionSchedule)) .
2843 (nat-eliminate
2844 (lambda unrestricted current : Nat . (family NvidiaSubmissionSchedule))
2845 (constructor NvidiaSubmissionSchedule NvidiaSubmissionScheduleEmpty)
2846 (lambda unrestricted p : Nat .
2847 (lambda unrestricted induction : (family NvidiaSubmissionSchedule) .
2848 (cgSubmissionThen
2849 (body (naturalSaturatingSubtract (naturalSaturatingSubtract count 1) p))
2850 induction)))
2851 count)))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.