Core.index_of: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/core.bend as Core
Lines 828-835 of bendtorch-core@0.1.0.0/src/shape/core.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&start_line=828&end_line=835

import Base

# Index rows are formed only below a nonzero output count. Every padded input
# extent is then 1 or the output extent, so no product exceeds that count.
def index_of(+left: Shape, +right: Shape, +output: Shape, empty: BoolCase<Nat.is_eq(elements(output), 0n)>) -> Index<extents(left), extents(right), extents(output)>:
  match empty:
    case BTrue{equal}:
      Unindexed{Equal.trans(Nat, 0n, elements(output), numel(extents(output)), Equal.sym(Nat, elements(output), 0n, equal_from(elements(output), 0n, equal)), elements_exact(output))}
    case BFalse{equal}:
      Indexed{index_of.rows(left, right, output, rank_dimensions(dimensions(output))), index_of.exact(left, right, output)}

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=BoolCase
  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/shape/core.bend&name=Shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=dimensions
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=elements
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=elements_exact
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=equal_from
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=extents
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=index_of.exact
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=index_of.rows
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=numel
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=rank_dimensions