ElementwiseWalkProof.cell_by_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 233-261 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=233&end_line=261

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

# With the slots `left_slot` and `right_slot` pick, the cell of a build is
# the cell with the walk.
def cell_by_same(+operation: Elementwise.Operation, -le: List<&2, Nat>, -re: List<&2, Nat>, -oe: List<&2, Nat>,
  +map: Shape.Index<le, re, oe>, inside: Bool, 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.cell_by(inside, left, right, operation, le, re, oe, map, position, la, ra) ==
    Elementwise.cell(operation, le, re, oe, map, position, la, ra, inside) : F32 & (Array<F32> & Array<F32>)}:
  match inside left right:
    case False{} left right:
      {==}
    case True{} Elementwise.OwnSlot{} Elementwise.OwnSlot{}:
      direct_same(operation, le, re, oe, map, Elementwise.OwnSlot{}, left_exact, Elementwise.OwnSlot{}, right_exact, position, la, ra)
    case True{} Elementwise.OwnSlot{} Elementwise.FirstSlot{}:
      direct_same(operation, le, re, oe, map, Elementwise.OwnSlot{}, left_exact, Elementwise.FirstSlot{}, right_exact, position, la, ra)
    case True{} Elementwise.OwnSlot{} Elementwise.WalkedSlot{}:
      direct_same(operation, le, re, oe, map, Elementwise.OwnSlot{}, left_exact, Elementwise.WalkedSlot{}, right_exact, position, la, ra)
    case True{} Elementwise.FirstSlot{} Elementwise.OwnSlot{}:
      direct_same(operation, le, re, oe, map, Elementwise.FirstSlot{}, left_exact, Elementwise.OwnSlot{}, right_exact, position, la, ra)
    case True{} Elementwise.FirstSlot{} Elementwise.FirstSlot{}:
      direct_same(operation, le, re, oe, map, Elementwise.FirstSlot{}, left_exact, Elementwise.FirstSlot{}, right_exact, position, la, ra)
    case True{} Elementwise.FirstSlot{} Elementwise.WalkedSlot{}:
      direct_same(operation, le, re, oe, map, Elementwise.FirstSlot{}, left_exact, Elementwise.WalkedSlot{}, right_exact, position, la, ra)
    case True{} Elementwise.WalkedSlot{} Elementwise.OwnSlot{}:
      direct_same(operation, le, re, oe, map, Elementwise.WalkedSlot{}, left_exact, Elementwise.OwnSlot{}, right_exact, position, la, ra)
    case True{} Elementwise.WalkedSlot{} Elementwise.FirstSlot{}:
      direct_same(operation, le, re, oe, map, Elementwise.WalkedSlot{}, left_exact, Elementwise.FirstSlot{}, right_exact, position, la, ra)
    case True{} Elementwise.WalkedSlot{} Elementwise.WalkedSlot{}:
      {==}

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=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_by
  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=right_slot
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_walk_proof.bend&name=direct_same