ReductionPROOF.success: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend as ReductionPROOF
Lines 704-714 of bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend&start_line=704&end_line=714

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

def success(-error: Data, -value: Type, result: Result<&2, &1, error, value>,
  -status: Totality.Status<error, value, result>) -> Totality.Success<error, value, result>:
  match result:
    case Fail{failure}:
      Totality.Success{
        {\{Totality.Status: successful => Empty.absurd({False{} == True{} : Bool}, Arith.clash(successful))} :
          Totality.Status<error, value, Fail{failure}> -> {False{} == True{} : Bool}}(status),
        {\{Totality.Status: successful => Empty.absurd(Totality.DoneWitness<error, value, Fail{failure}>, Arith.clash(successful))} :
          Totality.Status<error, value, Fail{failure}> -> Totality.DoneWitness<error, value, Fail{failure}>}(status)}
    case Done{returned}:
      Totality.Success{{==}, Totality.DoneWitness{returned, {==}}}

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=clash
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/math_totality.bend&name=DoneWitness
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/math_totality.bend&name=Status
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/math_totality.bend&name=Success