AlphaGitHub
Source/Packages

Std.List

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

306 lines19 declarations12.2 KiBSHA-256 6cdb3b134c6e
Download exact fileView at revisionf5034773ad4bb52133

def · lines 43–52

stdListHeadOr

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