AlphaGitHub
Source/Packages

Learning.DataParallel

packages/learning/src/Learning/DataParallel.alpha

672 lines35 declarations28.2 KiBSHA-256 f725f80cd07f
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 243–254

dataParallelSamplesOf

Full file
The samples one owner holds, in order (none for an owner past the list).
243def dataParallelSamplesOf =
244  (lambda erased contribution : Nat .
245    (lambda erased update : Nat .
246      (lambda unrestricted system : (family DataParallelSystem contribution update) .
247        (lambda unrestricted owner : Nat .
248          (stdListHeadOr
249            (family StdList (family StdList StdU64))
250            (constructor StdList StdListEmpty (family StdList StdU64))
251            (stdListDrop
252              (family StdList (family StdList StdU64))
253              owner
254              (dataParallelOwnerSamples contribution update system)))))))

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.