1485def deviceArenaRunsOf =
1486 (lambda unrestricted schedule : (family NvidiaLaunchSchedule) .
1487 (eliminate
1488 NvidiaLaunchSchedule
1489 (lambda unrestricted current : (family NvidiaLaunchSchedule) . (family DeviceArenaRuns))
1490 schedule
1491 (branch NvidiaLaunchScheduleEmpty . (constructor DeviceArenaRuns DeviceArenaRunsEnd))
1492 (branch
1493 NvidiaLaunchScheduleOne
1494 template
1495 .
1496 (constructor
1497 DeviceArenaRuns
1498 DeviceArenaRunsNext
1499 (deviceArenaLaunchIdentityOf (deviceArenaLaunchOf template))
1500 0
1501 1
1502 (constructor DeviceArenaRuns DeviceArenaRunsEnd)))
1503 (branch
1504 NvidiaLaunchScheduleAppend
1505 left
1506 right
1507 il
1508 ir
1509 .
1510 (deviceArenaRunsShifted
1511 0
1512 il
1513 (deviceArenaRunsShifted
1514 (nvidiaLaunchScheduleCount left)
1515 ir
1516 (constructor DeviceArenaRuns DeviceArenaRunsEnd))))
1517 (branch
1518 NvidiaLaunchScheduleRepeat
1519 count
1520 iteration
1521 body
1522 ib
1523 .
1524 (let unrestricted extent =
1525 (nvidiaLaunchScheduleCount body)
1526 in
1527 (nat-eliminate
1528 (lambda unrestricted remaining : Nat . (family DeviceArenaRuns))
1529 (constructor DeviceArenaRuns DeviceArenaRunsEnd)
1530 (lambda unrestricted p : Nat .
1531 (lambda unrestricted induction : (family DeviceArenaRuns) .
1532 (deviceArenaRunsShifted
1533 (naturalMultiply
1534 (naturalSaturatingSubtract (naturalSaturatingSubtract count 1) p)
1535 extent)
1536 ib
1537 induction)))
1538 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.