def success

bendtorch-core@0.1.0.0 · src/tensor/reduction_PROOF.bend:704

import Base
import bendtorch-core@0.1.0.0/src/tensor/math_totality.bend as Totality
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith

704def success(-error: Data, -value: Type, result: Result<&2, &1, error, value>,
705  -status: Totality.Status<error, value, result>) -> Totality.Success<error, value, result>:
706  match result:
707    case Fail{failure}:
708      Totality.Success{
709        {\{Totality.Status: successful => Empty.absurd({False{} == True{} : Bool}, Arith.clash(successful))} :
710          Totality.Status<error, value, Fail{failure}> -> {False{} == True{} : Bool}}(status),
711        {\{Totality.Status: successful => Empty.absurd(Totality.DoneWitness<error, value, Fail{failure}>, Arith.clash(successful))} :
712          Totality.Status<error, value, Fail{failure}> -> Totality.DoneWitness<error, value, Fail{failure}>}(status)}
713    case Done{returned}:
714      Totality.Success{{==}, Totality.DoneWitness{returned, {==}}}