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 89–104

stdListAppend

Full file
The left list followed by the right one. The right list is SHARED, not copied: only the left spine is rebuilt.
89def stdListAppend =
90  (lambda erased element : Type 0 .
91    (lambda unrestricted left : (family StdList element) .
92      (lambda unrestricted right : (family StdList element) .
93        (eliminate
94          StdList
95          (lambda unrestricted current : (family StdList element) . (family StdList element))
96          left
97          (branch StdListEmpty . right)
98          (branch
99            StdListCons
100            head
101            tail
102            induction
103            .
104            (constructor StdList StdListCons element head 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.