def finish_success

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

import Base
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
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

225def finish_success(pair: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic>,
226  -success: Totality.Success<pair>) -> Laws.Success<Broadcast.finish(pair)>:
227  ((input, zeros), result) = pair
228  match result:
229    case Fail{error}:
230      Laws.Success{Empty.absurd({False{} == True{} : Bool}, Arith.clash(
231        {\{Totality.Success: successful => successful} : Totality.Success<((input, zeros), Fail{error})> -> {False{} == True{} : Bool}}(success)))}
232    case Done{output}:
233      Laws.Success{{==}}