Source/Packages

Std.List

packages/foundation/standard/src/Std/List.alpha

361 lines21 declarations15.3 KiBSHA-256 b071be8610d6

def · lines 45–54

stdListHeadOr

Full file
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.