def successful_pair_mapping

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

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/elementwise.bend as Elementwise

990def successful_pair_mapping(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, -left: Core.Dynamic, -right: Core.Dynamic,
991  result: (Core.Dynamic & Core.Dynamic) & Result<&2, &1, Core.Error, Core.Dynamic>,
992  -meaning: Elementwise.LoopMeaning(operation, plan, left, right, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), result)) ->
993  Elementwise.MappingModel<operation, plan, left, right, result>:
994  (inputs, outcome) = result
995  match outcome:
996    case Fail{error}:
997      Elementwise.MappingModel{Unit{}}
998    case Done{output}:
999      Elementwise.MappingModel{index => bound => Pair.snd(Core.ObservationChecked(output, index),
1000        {Core.observe_dynamic(output, index) == Elementwise.expected(operation, plan, left, right, index) : Maybe<&2, F32>}, meaning(index)(bound))}