Source/Systems

Coppelius.Build.Graph

systems/coppelius/src/Coppelius/Build/Graph.alpha

3,461 lines536 declarations124.9 KiBSHA-256 6b9f923bd170

def · lines 1289–1300

cgFor

Full file
body 0, body 1, ..., body (count - 1)
1289def cgFor =
1290  (lambda unrestricted count : Nat .
1291    (lambda unrestricted body : (pi unrestricted index : Nat . (family NvidiaLaunchSchedule)) .
1292      (nat-eliminate
1293        (lambda unrestricted current : Nat . (family NvidiaLaunchSchedule))
1294        cgNothing
1295        (lambda unrestricted p : Nat .
1296          (lambda unrestricted induction : (family NvidiaLaunchSchedule) .
1297            (cgThen
1298              (body (naturalSaturatingSubtract (naturalSaturatingSubtract count 1) p))
1299              induction)))
1300        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.