Coercions and lists

Stream: new members

[Nick Pilotti]

Hello! Suppose I have an instance of a coercion for type A to type B. Is there a library function that will allow me to easily construct a coercion from list A to list B?

[Kyle Miller]

You can use list.map with coe to do the coercion, for example list.map coe xs if xs : list A. You might need a type hint like (list.map coe xs : list B) (or, if you want, list.map (coe : A -> B) xs)

[Kyle Miller]

You should also be able to use dot notation, for example xs.map coe

[Nick Pilotti]

Thank you!

[Eric Wieser]

Doesn't this exist as docs#lift_list?

[Eric Wieser]

You need to write the ↑ explicitly though