def converted_step_certificate

bendtorch-core@0.1.0.0 · src/tensor/core_PROOF.bend:634

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise

634def converted_step_certificate(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +cursor: Nat, +index: U32,
635  +equal: {True{} == Nat.is_eq(U32.to_nat(index), cursor) : Bool}, -original: Elementwise.State<Shape.output_shape(plan)>,
636  certificate: Elementwise.StepCertificate<operation, plan, index, original>) ->
637  Elementwise.ConvertedCertificate<operation, plan, cursor, index, Shape.BTrue{equal}, original>:
638  Elementwise.StepCertificate{result, exact, meaning} = certificate
639  match result:
640    case Elementwise.Stop{left, right, error}:
641      Elementwise.ConvertedCertificate{Elementwise.NaturalStop{left, right, error},
642        Equal.cong(Elementwise.Step<Shape.output_shape(plan)>, Elementwise.NaturalStep<Shape.output_shape(plan), cursor>,
643          step => Elementwise.natural_step_result(Shape.output_shape(plan), cursor, index, Lifecycle.natural_equal(U32.to_nat(index), cursor, equal), step),
644          Elementwise.Stop{left, right, error}, Elementwise.step(operation, plan, index, original), exact), Unit{}}
645    case Elementwise.Continue{state}:
646      Elementwise.ConvertedCertificate{Elementwise.NaturalContinue{state, index, Lifecycle.natural_equal(U32.to_nat(index), cursor, equal)},
647        Equal.cong(Elementwise.Step<Shape.output_shape(plan)>, Elementwise.NaturalStep<Shape.output_shape(plan), cursor>,
648          step => Elementwise.natural_step_result(Shape.output_shape(plan), cursor, index, Lifecycle.natural_equal(U32.to_nat(index), cursor, equal), step),
649          Elementwise.Continue{state}, Elementwise.step(operation, plan, index, original), exact), meaning}