AlphaGitHub
Source/Packages

Std.List

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

361 lines21 declarations15.3 KiBSHA-256 b071be8610d6
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 91–106

stdListAppend

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