def index_of.exact
bendtorch-core@0.1.0.0 · src/shape/core.bend:817
import bendtorch-core@0.1.0.0/src/shape/core.bend as Core
import Base
817def 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>}:
818 +lp = Nat.sub(rank_dimensions(dimensions(output)), rank_dimensions(dimensions(left)))
819 +rp = Nat.sub(rank_dimensions(dimensions(output)), rank_dimensions(dimensions(right)))
820 %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>}
821 %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>}
822 %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>}
823 %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>}
824 %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>}
825 %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>}
826 {==}