def lists_0

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

import Base

337def lists_0(-A: Data, +items: List<&2, A>, length: {List.length(&2, A, items) == 1n : Nat}) -> ListFacts<A, 1n, [0n], items>:
338  match items:
339    case Nil{}:
340      Empty.absurd(ListFacts<A, 1n, [0n], Nil{}>, nat_clash(0n, 1n, length, {==}))
341    case +x0 <> Nil{}:
342      Lists{{==}, {==}, {==}, {==}, {==}, {==}}
343    case +x0 <> +x1 <> +tail:
344      Empty.absurd(ListFacts<A, 1n, [0n], x0 <> x1 <> tail>, nat_clash(2n+List.length(&2, A, tail), 1n, length, {==}))