def lookup_complete

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

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

234def lookup_complete(-A: Data, +items: List<&2, A>, +index: Nat, bound: Shape.LT(index, List.length(&2, A, items))) -> Selected<A, items, index>:
235  match items index:
236    case Nil{} 0n:
237      match bound:
238    case Nil{} 1n+p:
239      match bound:
240    case +head <> tail 0n:
241      Selection{head, {==}}
242    case +head <> +tail 1n+p:
243      lookup_complete_step(A, head, tail, p, lookup_complete(A, tail, p, bound))