The first element, or the supplied default for an empty list.
45def stdListHeadOr =
46 (lambda erased element : Type 0 .
47 (lambda unrestricted fallback : element .
48 (lambda unrestricted values : (family StdList element) .
49 (eliminate
50 StdList
51 (lambda unrestricted current : (family StdList element) . element)
52 values
53 (branch StdListEmpty . fallback)
54 (branch StdListCons head tail induction . 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.