def natural_success
bendtorch-core@0.1.0.0 · src/tensor/elementwise_PROOF.bend:758
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/tensor/transform_PROOF.bend as TransformProof
import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
758def natural_success(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +cursor: Nat,
759 state: Elementwise.State<Shape.output_shape(plan)>,
760 -fits: FittingSources<plan, step_left_owner(Shape.output_shape(plan), Elementwise.Continue{state}), step_right_owner(Shape.output_shape(plan), Elementwise.Continue{state})>,
761 -inside: {Nat.is_lt(cursor, Shape.elements(Shape.output_shape(plan))) == True{} : Bool}) ->
762 NaturalSuccess<Shape.output_shape(plan), cursor, Elementwise.natural_step(operation, plan, cursor, state)>:
763 natural_decided_success(operation, plan, cursor, U32.from_nat(cursor), Shape.bool_case(Nat.is_eq(U32.to_nat(U32.from_nat(cursor)), cursor)), state, fits,
764 TransformProof.cursor_word_exact(Shape.output_shape(plan), cursor, Conversion.lt_le(cursor, Shape.elements(Shape.output_shape(plan)), inside)), inside)