AlphaGitHub
Source/Packages

Learning.ScaledProductUpdate

packages/learning/src/Learning/ScaledProductUpdate.alpha

66 lines3 declarations3.3 KiBSHA-256 bd32823ac4f3
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 21–31

scaledProductSlotsIndependent

Full file
21def scaledProductSlotsIndependent =
22  (lambda erased slots : Nat .
23    (lambda unrestricted state : (family StdFin slots) .
24      (lambda unrestricted coefficient : (family StdFin slots) .
25        (lambda unrestricted left : (family StdFin slots) .
26          (lambda unrestricted right : (family StdFin slots) .
27            (naturalAnd
28              (pointwiseSlotsSeparate slots state coefficient)
29              (naturalAnd
30                (pointwiseSlotsSeparate slots state left)
31                (pointwiseSlotsSeparate slots state right))))))))

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.