AlphaGitHub
Source/Packages

Accelerator.SM121.Lowering

packages/hardware/architectures/nvidia-sm121/src/Accelerator/SM121/Lowering.alpha

2,621 lines365 declarations134.1 KiBSHA-256 b7b3bbc05e9c
Download exact fileView at revisionf5034773ad4bb52133

def · lines 1695–1713

sm121LowerPredicateReady

Full file
1695def sm121LowerPredicateReady =
1696  (lambda unrestricted pending : (family SM121LowerPending) .
1697    (lambda unrestricted predicate : Nat .
1698      (eliminate
1699        SM121LowerPending
1700        (lambda unrestricted current : (family SM121LowerPending) . Nat)
1701        pending
1702        (branch SM121LowerPendingEnd . zero)
1703        (branch SM121LowerPendingNext entry time class tail induction .
1704          (nat-eliminate (lambda unrestricted current : Nat . Nat)
1705            induction
1706            (lambda unrestricted flagPredecessor : Nat . (lambda unrestricted flagRest : Nat . (nat-add time sm121LowerPredicateLatency)))
1707            (nat-eliminate (lambda unrestricted current : Nat . Nat)
1708              (nat-eliminate (lambda unrestricted current : Nat . Nat)
1709                (succ zero)
1710                (lambda unrestricted flagPredecessor : Nat . (lambda unrestricted flagRest : Nat . zero))
1711                (nat-less-than predicate entry))
1712              (lambda unrestricted flagPredecessor : Nat . (lambda unrestricted flagRest : Nat . zero))
1713              (nat-less-than entry predicate)))))))

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.