The list in the opposite order.
107def stdListReverse =
108 (lambda erased element : Type 0 .
109 (lambda unrestricted values : (family StdList element) .
110 (app
111 (eliminate
112 StdList
113 (lambda unrestricted current : (family StdList element) .
114 (pi unrestricted accumulator : (family StdList element) . (family StdList element)))
115 values
116 (branch
117 StdListEmpty
118 .
119 (lambda unrestricted accumulator : (family StdList element) . accumulator))
120 (branch
121 StdListCons
122 head
123 tail
124 induction
125 .
126 (lambda unrestricted accumulator : (family StdList element) .
127 (induction (constructor StdList StdListCons element head accumulator)))))
128 (constructor StdList StdListEmpty element))))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.