Core.Index: type of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/core.bend as Core
Lines 810-812 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=810&end_line=812

import Base

type Index<-left: List<&2, Nat>, -right: List<&2, Nat>, -output: List<&2, Nat>> is Data:
  Indexed{rows: List<&2, Row>, exact: {rows == index_table(left, right, output) : List<&2, Row>}}
  Unindexed{zero: {0n == numel(output) : Nat}}

Uses (5):
  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=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=index_table
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=numel