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