AxisAlgebra.gather_naturals: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend as AxisAlgebra
Lines 283-296 of bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&start_line=283&end_line=296

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/axis_spec.bend as Axis

def gather_naturals(+axes: List<&2, Nat>, +items: List<&2, U32>) ->
  {natural_values(Axis.gather(U32, items, axes)) == Axis.gather(Nat, Shape.naturals(items), axes) : Maybe<&2, List<&2, Nat>>}:
  match axes:
    case Nil{}:
      {==}
    case +head <> +tail:
      %Equal.sym(Maybe<&2, List<&2, Nat>>, natural_values(Axis.prepend(U32, Axis.lookup(U32, items, head), Axis.gather(U32, items, tail))),
        Axis.prepend(Nat, natural_value(Axis.lookup(U32, items, head)), natural_values(Axis.gather(U32, items, tail))), prepend_naturals(Axis.lookup(U32, items, head), Axis.gather(U32, items, tail))) :
        {_ == Axis.prepend(Nat, Axis.lookup(Nat, Shape.naturals(items), head), Axis.gather(Nat, Shape.naturals(items), tail)) : Maybe<&2, List<&2, Nat>>}
      %Equal.sym(Maybe<&2, Nat>, natural_value(Axis.lookup(U32, items, head)), Axis.lookup(Nat, Shape.naturals(items), head), lookup_naturals(items, head)) :
        {Axis.prepend(Nat, _, natural_values(Axis.gather(U32, items, tail))) == Axis.gather(Nat, Shape.naturals(items), head <> tail) : Maybe<&2, List<&2, Nat>>}
      %Equal.sym(Maybe<&2, List<&2, Nat>>, natural_values(Axis.gather(U32, items, tail)), Axis.gather(Nat, Shape.naturals(items), tail), gather_naturals(tail, items)) :
        {Axis.prepend(Nat, Axis.lookup(Nat, Shape.naturals(items), head), _) == Axis.gather(Nat, Shape.naturals(items), head <> tail) : Maybe<&2, List<&2, Nat>>}
      {==}

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=Maybe
  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=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/tensor/axis_algebra.bend&name=lookup_naturals
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=natural_value
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=natural_values
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=prepend_naturals
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_spec.bend&name=gather
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_spec.bend&name=lookup
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_spec.bend&name=prepend