def finish_retains

bendtorch-core@0.1.0.0 · src/autograd/broadcast_PROOF.bend:28

import Base
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/elementwise_totality.bend as Totality
import bendtorch-core@0.1.0.0/src/autograd/broadcast.bend as Broadcast
import bendtorch-core@0.1.0.0/src/autograd/broadcast_LAWS.bend as Laws

28def finish_retains(-input: Core.Dynamic, -right: Core.Dynamic,
29  pair: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic>,
30  -retention: Totality.Retention<input, right, pair>) -> Laws.Retained<input, Broadcast.finish(pair)>:
31  ((left, other), result) = pair
32  match result:
33    case Fail{error}:
34      Laws.Retained{{\{Totality.Retention: l => r => l} : Totality.Retention<input, right, ((left, other), Fail{error})> -> Totality.SameSource(input, left)}(retention)}
35    case Done{output}:
36      Laws.Retained{{\{Totality.Retention: l => r => l} : Totality.Retention<input, right, ((left, other), Done{output})> -> Totality.SameSource(input, left)}(retention)}