def order_naturals

bendtorch-core@0.1.0.0 · src/tensor/axis_algebra.bend:306

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

306def order_naturals(+axes: List<&2, Nat>, +items: List<&2, U32>) ->
307  {Shape.naturals(Axis.order(U32, items, axes)) == Axis.order(Nat, Shape.naturals(items), axes) : List<&2, Nat>}:
308  Equal.trans(List<&2, Nat>, Shape.naturals(Axis.order(U32, items, axes)), Axis.values(Nat, natural_values(Axis.gather(U32, items, axes))),
309    Axis.order(Nat, Shape.naturals(items), axes), values_naturals(Axis.gather(U32, items, axes)),
310    Equal.cong(Maybe<&2, List<&2, Nat>>, List<&2, Nat>, result => Axis.values(Nat, result), natural_values(Axis.gather(U32, items, axes)),
311      Axis.gather(Nat, Shape.naturals(items), axes), gather_naturals(axes, items)))