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 32–40

stdListLength

Full file
The number of elements.
32def stdListLength =
33  (lambda erased element : Type 0 .
34    (lambda unrestricted values : (family StdList element) .
35      (eliminate
36        StdList
37        (lambda unrestricted current : (family StdList element) . Nat)
38        values
39        (branch StdListEmpty . zero)
40        (branch StdListCons head tail induction . (succ induction)))))

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.