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