Core.index_of.exact: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/core.bend as Core
Lines 817-826 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=817&end_line=826

import Base

def index_of.exact(+left: Shape, +right: Shape, +output: Shape) -> {index_of.rows(left, right, output, rank_dimensions(dimensions(output))) == index_table(extents(left), extents(right), extents(output)) : List<&2, Row>}:
  +lp = Nat.sub(rank_dimensions(dimensions(output)), rank_dimensions(dimensions(left)))
  +rp = Nat.sub(rank_dimensions(dimensions(output)), rank_dimensions(dimensions(right)))
  %Equal.sym(List<&2, Row>, index_rows_words(pad_words(lp, dimensions(left)), pad_words(rp, dimensions(right)), dimensions(output)), index_rows(naturals(pad_words(lp, dimensions(left))), naturals(pad_words(rp, dimensions(right))), extents(output)), index_rows_spec(pad_words(lp, dimensions(left)), pad_words(rp, dimensions(right)), dimensions(output))) : {_ == index_table(extents(left), extents(right), extents(output)) : List<&2, Row>}
  %Equal.sym(List<&2, Nat>, naturals(pad_words(lp, dimensions(left))), pad(lp, extents(left)), naturals_pad(lp, dimensions(left))) : {index_rows(_, naturals(pad_words(rp, dimensions(right))), extents(output)) == index_table(extents(left), extents(right), extents(output)) : List<&2, Row>}
  %Equal.sym(List<&2, Nat>, naturals(pad_words(rp, dimensions(right))), pad(rp, extents(right)), naturals_pad(rp, dimensions(right))) : {index_rows(pad(lp, extents(left)), _, extents(output)) == index_table(extents(left), extents(right), extents(output)) : List<&2, Row>}
  %Equal.sym(Nat, rank_dimensions(dimensions(output)), List.length(&2, Nat, extents(output)), rank_naturals(dimensions(output))) : {index_rows(pad(Nat.sub(_, rank_dimensions(dimensions(left))), extents(left)), pad(Nat.sub(_, rank_dimensions(dimensions(right))), extents(right)), extents(output)) == index_table(extents(left), extents(right), extents(output)) : List<&2, Row>}
  %Equal.sym(Nat, rank_dimensions(dimensions(left)), List.length(&2, Nat, extents(left)), rank_naturals(dimensions(left))) : {index_rows(pad(Nat.sub(List.length(&2, Nat, extents(output)), _), extents(left)), pad(Nat.sub(List.length(&2, Nat, extents(output)), rank_dimensions(dimensions(right))), extents(right)), extents(output)) == index_table(extents(left), extents(right), extents(output)) : List<&2, Row>}
  %Equal.sym(Nat, rank_dimensions(dimensions(right)), List.length(&2, Nat, extents(right)), rank_naturals(dimensions(right))) : {index_rows(pad(Nat.sub(List.length(&2, Nat, extents(output)), List.length(&2, Nat, extents(left))), extents(left)), pad(Nat.sub(List.length(&2, Nat, extents(output)), _), extents(right)), extents(output)) == index_table(extents(left), extents(right), extents(output)) : List<&2, Row>}
  {==}

Uses (20):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Row
  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=extents
  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=index_rows
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=index_rows_spec
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=index_rows_words
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=index_table
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=naturals
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=naturals_pad
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=pad
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=pad_words
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=rank_dimensions
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=rank_naturals