def lookup

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

import Base
import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout
import bendtorch-core@0.1.0.0/src/tensor/axis_spec.bend as Axis

10def lookup(+values: List<&2, U32>, +index: Nat) -> {Layout.lookup(values, index) == Axis.lookup(U32, values, index) : Maybe<&2, U32>}:
11  match values index:
12    case Nil{} 0n:
13      {==}
14    case Nil{} 1n+p:
15      {==}
16    case head <> tail 0n:
17      {==}
18    case head <> +tail 1n+p:
19      lookup(tail, p)