The first element as an option, so the empty case is visible in the type.
57def stdListHead =
58 (lambda erased element : Type 0 .
59 (lambda unrestricted values : (family StdList element) .
60 (eliminate
61 StdList
62 (lambda unrestricted current : (family StdList element) . (family StdOption element))
63 values
64 (branch StdListEmpty . (constructor StdOption StdNone element))
65 (branch StdListCons head tail induction . (constructor StdOption StdSome element head)))))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.