def prefix_equal

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

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/word_injective.bend as Injective
import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise

785def prefix_equal(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan,
786  -original_left: Core.Dynamic, -original_right: Core.Dynamic, +cursor: Nat, +index: U32,
787  -after: Core.Tensor<Shape.output_shape(plan)>, converted: {U32.to_nat(index) == cursor : Nat},
788  checked: Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), after}, index),
789  observed: {Core.observe(Shape.output_shape(plan), after, index) == Elementwise.expected(operation, plan, original_left, original_right, index) : Maybe<&2, F32>},
790  +other: U32, equal: {U32.to_nat(other) == cursor : Nat}) ->
791  Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), after}, other) &
792    {Core.observe(Shape.output_shape(plan), after, other) == Elementwise.expected(operation, plan, original_left, original_right, other) : Maybe<&2, F32>}:
793  %Injective.u32_natural_injective(index, other)(Equal.trans(Nat, U32.to_nat(index), cursor, U32.to_nat(other), converted,
794    Equal.sym(Nat, U32.to_nat(other), cursor, equal))) :
795    Core.ObservationChecked(Core.Packed{Shape.output_shape(plan), after}, _) &
796      {Core.observe(Shape.output_shape(plan), after, _) == Elementwise.expected(operation, plan, original_left, original_right, _) : Maybe<&2, F32>}
797  (checked, observed)