CorePROOF.expected_same_indices: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend as CorePROOF
Lines 725-745 of bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&start_line=725&end_line=745

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

def expected_same_indices(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +index: U32,
  -original_left: Core.Dynamic, -original_right: Core.Dynamic, -left: Core.Dynamic, -right: Core.Dynamic,
  -left_same: Elementwise.SameSource(original_left, left), -right_same: Elementwise.SameSource(original_right, right),
  result: Result<&2, &1, Core.Error, U32 & U32>,
  -exact: {result == Elementwise.input_indices(plan, index) : Result<&2, &1, Core.Error, U32 & U32>}) ->
  ExpectedSame<operation, plan, index, original_left, original_right, left, right>:
  match result:
    case Fail{error}:
      ExpectedSame{
        %exact : {Elementwise.expected_indices(operation, left, right, _) == Elementwise.expected_indices(operation, original_left, original_right, _) : Maybe<&2, F32>}
        {==}}
    case Done{indices}:
      (+left_index, +right_index) = indices
      ExpectedSame{
        %exact : {Elementwise.expected_indices(operation, left, right, _) == Elementwise.expected_indices(operation, original_left, original_right, _) : Maybe<&2, F32>}
        Equal.trans(Maybe<&2, F32>, Elementwise.expected_left(operation, right, right_index, Core.checked_observe_dynamic(left, left_index)),
          Elementwise.expected_left(operation, right, right_index, Core.checked_observe_dynamic(original_left, left_index)),
          Elementwise.expected_left(operation, original_right, right_index, Core.checked_observe_dynamic(original_left, left_index)),
          Equal.cong(Maybe<&2, F32>, Maybe<&2, F32>, value => Elementwise.expected_left(operation, right, right_index, value),
            Core.checked_observe_dynamic(left, left_index), Core.checked_observe_dynamic(original_left, left_index), left_same(left_index)),
          expected_left_same(operation, right, original_right, right_index, Core.checked_observe_dynamic(original_left, left_index), right_same(right_index)))}

Uses (19):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=BroadcastPlan
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Dynamic
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Error
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=checked_observe_dynamic
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=ExpectedSame
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=expected_left_same
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=Operation
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=SameSource
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=expected_indices
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=expected_left
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=input_indices