ElementwiseWalkProof.direct_same: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/elementwise_walk_proof.bend as ElementwiseWalkProof
Lines 210-231 of bendtorch-core@0.1.0.0/src/tensor/elementwise_walk_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_walk_proof.bend&start_line=210&end_line=231

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

# An inside cell whose slots are known is the cell with the walk.
def direct_same(+operation: Elementwise.Operation, -le: List<&2, Nat>, -re: List<&2, Nat>, -oe: List<&2, Nat>,
  +map: Shape.Index<le, re, oe>, +left: Elementwise.Slot, +left_exact: {left == Elementwise.left_slot(le, re, oe, map) : Elementwise.Slot},
  +right: Elementwise.Slot, +right_exact: {right == Elementwise.right_slot(le, re, oe, map) : Elementwise.Slot},
  +position: Nat, -la: Array<F32>, -ra: Array<F32>) ->
  {Elementwise.direct_cell(operation, left_at(left, le, re, oe, map, position), right_at(right, le, re, oe, map, position), la, ra) ==
    Elementwise.cell(operation, le, re, oe, map, position, la, ra, True{}) : F32 & (Array<F32> & Array<F32>)}:
  +lw = Elementwise.left_walk(le, re, oe, map, position)
  +rw = Elementwise.right_walk(le, re, oe, map, position)
  %Equal.sym(Nat, left_at(left, le, re, oe, map, position), lw,
    %Equal.sym(Elementwise.Slot, left, Elementwise.left_slot(le, re, oe, map), left_exact) :
      {left_at(_, le, re, oe, map, position) == lw : Nat}
    left_index(le, re, oe, map, position)) :
    {Elementwise.cell_left(operation, ra, U32.from_nat(right_at(right, le, re, oe, map, position)), Array.get(F32, la, U32.from_nat(_))) ==
      Elementwise.cell_left(operation, ra, U32.from_nat(rw), Array.get(F32, la, U32.from_nat(lw))) : F32 & (Array<F32> & Array<F32>)}
  %Equal.sym(Nat, right_at(right, le, re, oe, map, position), rw,
    %Equal.sym(Elementwise.Slot, right, Elementwise.right_slot(le, re, oe, map), right_exact) :
      {right_at(_, le, re, oe, map, position) == rw : Nat}
    right_index(le, re, oe, map, position)) :
    {Elementwise.cell_left(operation, ra, U32.from_nat(_), Array.get(F32, la, U32.from_nat(lw))) ==
      Elementwise.cell_left(operation, ra, U32.from_nat(rw), Array.get(F32, la, U32.from_nat(lw))) : F32 & (Array<F32> & Array<F32>)}
  {==}

Uses (23):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.get
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Index
  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=Slot
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=cell
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=cell_left
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=direct_cell
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=left_slot
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=left_walk
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=right_slot
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=right_walk
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_walk_proof.bend&name=left_at
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_walk_proof.bend&name=left_index
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_walk_proof.bend&name=right_at
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_walk_proof.bend&name=right_index