PermuteBuildProof.lookup_digits: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend as PermuteBuildProof
Lines 69-86 of bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&start_line=69&end_line=86

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

# Coordinate k of `Shape.digits(dims, x)` is what the pick of k computes.
def lookup_digits(+dims: List<&2, Nat>, +x: Nat, +k: Nat) ->
  {Axis.lookup(U32, Shape.words(Shape.digits(dims, x)), k) == coordinate_of(Build.pick_at(dims, k), x) : Maybe<&2, U32>}:
  match dims:
    case Nil{}:
      {==}
    case +head <> +tail:
      match k:
        case 0n:
          {==}
        case 1n+j:
          Equal.trans(Maybe<&2, U32>, Axis.lookup(U32, Shape.words(Shape.digits(tail, Nat.mod(x, Shape.numel(tail)))), j),
            coordinate_of(Build.pick_at(tail, j), Nat.mod(x, Shape.numel(tail))),
            coordinate_of(Build.widen(Shape.numel(tail), Build.pick_at(tail, j)), x),
            lookup_digits(tail, Nat.mod(x, Shape.numel(tail)), j),
            Equal.sym(Maybe<&2, U32>, coordinate_of(Build.widen(Shape.numel(tail), Build.pick_at(tail, j)), x),
              coordinate_of(Build.pick_at(tail, j), Nat.mod(x, Shape.numel(tail))),
              widen_coordinate(Shape.numel(tail), Build.pick_at(tail, j), x)))

Uses (15):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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=Nat.mod
  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=digits
  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=words
  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/permute_build.bend&name=pick_at
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build.bend&name=widen
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=coordinate_of
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend&name=widen_coordinate