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