PermuteBuild.pick_at: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/permute_build.bend as PermuteBuild
Lines 37-48 of bendtorch-core@0.1.0.0/src/tensor/permute_build.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build.bend&start_line=37&end_line=48

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

# The pick of coordinate k of `Shape.digits(dims, x)`; None past the last
# dimension.
def pick_at(+dims: List<&2, Nat>, k: Nat) -> Maybe<&2, Pick>:
  match dims:
    case Nil{}:
      None{}
    case head <> tail:
      match k:
        case 0n:
          Some{Pick{Nil{}, Shape.numel(tail)}}
        case 1n+j:
          widen(Shape.numel(tail), pick_at(tail, j))

Uses (6):
  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=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/tensor/permute_build.bend&name=Pick
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build.bend&name=widen