Source/Systems

Coppelius.Build.NativeHost

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

677 lines91 declarations41.8 KiBSHA-256 492ff96faac5

def · lines 410–422

coppeliusRunPeriods

Full file
410def coppeliusRunPeriods =
411  (lambda unrestricted entries : Bytes .
412    (lambda unrestricted adamW : (family NativePhysicalCommands) .
413      (lambda unrestricted tail : (family NvidiaPlanHostSteps) .
414        (app
415          (nat-eliminate
416            (lambda unrestricted current : Nat . (pi unrestricted after : (family NvidiaPlanHostSteps) . (family NvidiaPlanHostSteps)))
417            (lambda unrestricted after : (family NvidiaPlanHostSteps) . after)
418            (lambda unrestricted p : Nat .
419              (lambda unrestricted induction : (pi unrestricted after : (family NvidiaPlanHostSteps) . (family NvidiaPlanHostSteps)) .
420                (lambda unrestricted after : (family NvidiaPlanHostSteps) . (induction (coppeliusPeriod entries adamW p after)))))
421            coppeliusRunPublications)
422          tail))))

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.