def select_digits

bendtorch-core@0.1.0.0 · src/tensor/permute_build_proof.bend:88

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
import bendtorch-core@0.1.0.0/src/tensor/permute_build.bend as Build

88def select_digits(+dims: List<&2, Nat>, +x: Nat, +position: Maybe<&2, Nat>) ->
89  {Axis.select(U32, Shape.words(Shape.digits(dims, x)), position) == coordinate_of(Build.located(dims, position), x) : Maybe<&2, U32>}:
90  match position:
91    case None{}:
92      {==}
93    case Some{+k}:
94      lookup_digits(dims, x, k)