def lists_empty

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

import Base

312def lists_empty(-A: Data, +items: List<&2, A>, length: {List.length(&2, A, items) == 0n : Nat}) -> ListFacts<A, 0n, Nil{}, items>:
313  match items:
314    case Nil{}:
315      Lists{{==}, {==}, {==}, {==}, {==}, {==}}
316    case +x0 <> +tail:
317      Empty.absurd(ListFacts<A, 0n, Nil{}, x0 <> tail>, nat_clash(1n+List.length(&2, A, tail), 0n, length, {==}))