AlphaGitHub
Source/Packages

Runtime.NativeDataParallel

packages/execution/src/Runtime/NativeDataParallel.alpha

1,529 lines92 declarations70.3 KiBSHA-256 a009e951c1b2
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 731–744

dpApply

Full file
Combine arithmetic: out_i = left_i + right_i for every numerator word and the mass, each separately rounded.
731def dpApply =
732  (lambda unrestricted c : Nat .
733    (lambda unrestricted u : Nat .
734      (lambda unrestricted system : (family DataParallelSystem c u) .
735        (lambda unrestricted out : Nat .
736          (lambda unrestricted left : Nat .
737            (lambda unrestricted right : Nat .
738              (dpEach
739                (succ (dpK c u system))
740                (lambda unrestricted index : Nat .
741                  (dpAdd
742                    (nativePointwiseAt out index)
743                    (nativePointwiseAt left index)
744                    (nativePointwiseAt right index))))))))))

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.