Everything after the first element; the empty list has an empty tail.
66def stdListTail =
67 (lambda erased element : Type 0 .
68 (lambda unrestricted values : (family StdList element) .
69 (eliminate
70 StdList
71 (lambda unrestricted current : (family StdList element) . (family StdList element))
72 values
73 (branch StdListEmpty . (constructor StdList StdListEmpty element))
74 (branch StdListCons head tail induction . tail))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.