One prediction depends on both parameter owners. No participant can train
its coordinate from its own prediction alone: its adjoint requires the
residual of the sum. Device arithmetic is a separate admitted realization.
12def coordinatePrediction =
13 (lambda erased value : Type 0 .
14 (lambda unrestricted add : (pi unrestricted left : value . (pi unrestricted right : value . value)) .
15 (lambda unrestricted multiply : (pi unrestricted left : value . (pi unrestricted right : value . value)) .
16 (lambda unrestricted leftWeight : value .
17 (lambda unrestricted rightWeight : value .
18 (lambda unrestricted leftInput : value .
19 (lambda unrestricted rightInput : value .
20 (add (multiply leftWeight leftInput) (multiply rightWeight rightInput)))))))))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.