map over a list but have access to membership property

Stream: general

[Frederick Pu]

is there any way to do List.map but in the function you have access to a : \alpha as well a proof that a is the in the list.

something like:

List.map' (l : List \alpha) (f : \sigma x, x \in l \r \beta) : List \beta := sorry

[Henrik Böving]

Use List.attach and List.map

[Yakov Pechersky]

Or, docs#List.pmap for that in one go. That being said, the way that List.attach is implemented, attach then map will be the same performance as pmap.