---- the assembly combine ----
An offered value is the k parameters followed by k ownership words (1 for
an owned coordinate). Combining selects, coordinate by coordinate, the
right operand's parameter where it owns the coordinate and the left
operand's otherwise; two owners for one coordinate refuse.
409def dpoOfferBytes =
410 (lambda unrestricted c : Nat .
411 (lambda unrestricted u : Nat .
412 (lambda unrestricted system : (family DataParallelSystem c u) .
413 (naturalMultiply dpWord (naturalMultiply 2 (dpK c u 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.