CorePROOF.expected_value: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend as CorePROOF
Lines 400-413 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=400&end_line=413

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_value(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +index: U32, -left: Core.Dynamic, -right: Core.Dynamic,
  +left_index: U32, +right_index: U32, +left_value: F32, +right_value: F32,
  -indices_exact: {Done{(left_index, right_index)} == Elementwise.input_indices(plan, index) : Result<&2, &1, Core.Error, U32 & U32>},
  left_model: ReadValueModel<left, left_index, left_value>, right_model: ReadValueModel<right, right_index, right_value>) ->
  ExpectedValue<operation, plan, index, left, right, left_value, right_value>:
  ReadValueModel{left_equal} = left_model
  ReadValueModel{right_equal} = right_model
  ExpectedValue{
    %indices_exact : {Some{Elementwise.scalar(operation, left_value, right_value)} == Elementwise.expected_indices(operation, left, right, _) : Maybe<&2, F32>}
    %Equal.sym(Maybe<&2, F32>, Core.checked_observe_dynamic(left, left_index), Some{left_value}, left_equal) :
      {Some{Elementwise.scalar(operation, left_value, right_value)} == Elementwise.expected_left(operation, right, right_index, _) : Maybe<&2, F32>}
    %Equal.sym(Maybe<&2, F32>, Core.checked_observe_dynamic(right, right_index), Some{right_value}, right_equal) :
      {Some{Elementwise.scalar(operation, left_value, right_value)} == Elementwise.expected_right(operation, left_value, _) : Maybe<&2, F32>}
    {==}}

Uses (19):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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=ExpectedValue
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=ReadValueModel
  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=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=expected_right
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=input_indices
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=scalar