def natural_result_success
bendtorch-core@0.1.0.0 · src/tensor/elementwise_PROOF.bend:731
import bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend as ElementwisePROOF
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
731def natural_result_success(-shape: Shape.Shape, -cursor: Nat, -index: U32, -exact: {U32.to_nat(index) == cursor : Nat},
732 result: Elementwise.Step<shape>, -successful: {step_succeeded(shape, result) == True{} : Bool}) ->
733 NaturalSuccess<shape, cursor, Elementwise.natural_step_result(shape, cursor, index, exact, result)>:
734 match result:
735 case Elementwise.Stop{left, right, error}:
736 NaturalSuccess{Empty.absurd({False{} == True{} : Bool}, Arith.clash(successful))}
737 case Elementwise.Continue{state}:
738 NaturalSuccess{{==}}