---- the schedule as written ----
385def deviceArenaSpansOf =
386 (lambda unrestricted patches : (family NvidiaParameterPatches) .
387 (eliminate
388 NvidiaParameterPatches
389 (lambda unrestricted current : (family NvidiaParameterPatches) . (family DeviceArenaSpans))
390 patches
391 (branch NvidiaParameterPatchesEnd . (constructor DeviceArenaSpans DeviceArenaSpansEnd))
392 (branch
393 NvidiaParameterPatchesNext
394 head
395 tail
396 induction
397 .
398 (eliminate
399 NvidiaParameterPatch
400 (lambda unrestricted current : (family NvidiaParameterPatch) . (family DeviceArenaSpans))
401 head
402 (branch
403 NvidiaParameterPatchValue
404 offset
405 value
406 .
407 (let unrestricted word =
408 (modelWord64Natural value)
409 in
410 (constructor
411 DeviceArenaSpans
412 DeviceArenaSpansNext
413 offset
414 (constructor
415 DeviceArenaIntervals
416 DeviceArenaIntervalsNext
417 word
418 word
419 (constructor DeviceArenaIntervals DeviceArenaIntervalsEnd))
420 0
421 0
422 1
423 0
424 (constructor DeviceArenaOrdinals DeviceArenaOrdinalsEnd)
425 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.