BroadcastPROOF.keep_left_expected: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/broadcast_PROOF.bend as BroadcastPROOF
Lines 71-80 of bendtorch-core@0.1.0.0/src/autograd/broadcast_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/broadcast_PROOF.bend&start_line=71&end_line=80

import Base
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 keep_left_expected(-right: Core.Dynamic, -right_index: U32, +left: Maybe<&2, F32>, -value: F32,
  -present: {Some{value} == Core.checked_observe_dynamic(right, right_index) : Maybe<&2, F32>}) ->
  Holds<{Elementwise.expected_left(Elementwise.KeepLeft{}, right, right_index, left) == left : Maybe<&2, F32>}>:
  match left:
    case None{}:
      Holds{{==}}
    case Some{+found}:
      Holds{
        %present : {Elementwise.expected_right(Elementwise.KeepLeft{}, found, _) == Some{found} : Maybe<&2, F32>}
        {==}}

Uses (9):
  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=U32
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/broadcast_PROOF.bend&name=Holds
  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=checked_observe_dynamic
  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_left
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=expected_right