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

import Base

def index_rows_spec(+left: List<&2, U32>, +right: List<&2, U32>, +output: List<&2, U32>) -> {index_rows_words(left, right, output) == index_rows(naturals(left), naturals(right), naturals(output)) : List<&2, Row>}:
  match left right output:
    case +lh <> +lt +rh <> +rt +oh <> +ot:
      %Equal.sym(Nat, numel_words(ot), numel(naturals(ot)), numel_words_spec(ot)) : {Row{_, broadcast_index(U32.to_nat(lh), numel_words(lt)), broadcast_index(U32.to_nat(rh), numel_words(rt))} <> index_rows_words(lt, rt, ot) == index_rows(naturals(lh <> lt), naturals(rh <> rt), naturals(oh <> ot)) : List<&2, Row>}
      %Equal.sym(Nat, numel_words(lt), numel(naturals(lt)), numel_words_spec(lt)) : {Row{numel(naturals(ot)), broadcast_index(U32.to_nat(lh), _), broadcast_index(U32.to_nat(rh), numel_words(rt))} <> index_rows_words(lt, rt, ot) == index_rows(naturals(lh <> lt), naturals(rh <> rt), naturals(oh <> ot)) : List<&2, Row>}
      %Equal.sym(Nat, numel_words(rt), numel(naturals(rt)), numel_words_spec(rt)) : {Row{numel(naturals(ot)), broadcast_index(U32.to_nat(lh), numel(naturals(lt))), broadcast_index(U32.to_nat(rh), _)} <> index_rows_words(lt, rt, ot) == index_rows(naturals(lh <> lt), naturals(rh <> rt), naturals(oh <> ot)) : List<&2, Row>}
      %Equal.sym(List<&2, Row>, index_rows_words(lt, rt, ot), index_rows(naturals(lt), naturals(rt), naturals(ot)), index_rows_spec(lt, rt, ot)) : {Row{numel(naturals(ot)), broadcast_index(U32.to_nat(lh), numel(naturals(lt))), broadcast_index(U32.to_nat(rh), numel(naturals(rt)))} <> _ == index_rows(naturals(lh <> lt), naturals(rh <> rt), naturals(oh <> ot)) : List<&2, Row>}
      {==}
    case Nil{} right output:
      {==}
    case lh <> lt Nil{} output:
      {==}
    case lh <> lt rh <> rt Nil{}:
      {==}

Uses (13):
  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=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_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=broadcast_index
  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_words
  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=numel
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=numel_words
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=numel_words_spec