Every element transformed, in order.
133def stdListMap =
134 (lambda erased element : Type 0 .
135 (lambda erased target : Type 0 .
136 (lambda unrestricted transform : (pi unrestricted value : element . target) .
137 (lambda unrestricted values : (family StdList element) .
138 (eliminate
139 StdList
140 (lambda unrestricted current : (family StdList element) . (family StdList target))
141 values
142 (branch StdListEmpty . (constructor StdList StdListEmpty target))
143 (branch
144 StdListCons
145 head
146 tail
147 induction
148 .
149 (constructor StdList StdListCons target (transform 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.