AlphaGitHub
Source/Packages

Realization.Nvidia.SM86.AdamWHalfSM86

packages/realizations/cooperative/nvidia-sm86/src/Realization/Nvidia/SM86/AdamWHalfSM86.alpha

428 lines73 declarations26.3 KiBSHA-256 9692515bc485
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 233–240

ahwPredicate

Full file
233def ahwPredicate = (lambda unrestricted q : Nat .
234  (nat-eliminate (lambda unrestricted n : Nat . (family SM86Predicate)) saP0
235    (lambda unrestricted p : Nat . (lambda unrestricted ignored : (family SM86Predicate) .
236      (nat-eliminate (lambda unrestricted n : Nat . (family SM86Predicate)) (constructor SM86Predicate SM86Predicate2)
237        (lambda unrestricted p2 : Nat . (lambda unrestricted ignored2 : (family SM86Predicate) .
238          (nat-eliminate (lambda unrestricted n : Nat . (family SM86Predicate)) (constructor SM86Predicate SM86Predicate3)
239            (lambda unrestricted p3 : Nat . (lambda unrestricted ignored3 : (family SM86Predicate) .
240              (constructor SM86Predicate SM86Predicate4))) p2))) p))) q))

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.