Zulip Chat Archive

Stream: new members

Topic: Coercions and lists


Nick Pilotti (Sep 02 2022 at 02:44):

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 (Sep 02 2022 at 02:46):

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 (Sep 02 2022 at 02:46):

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

Nick Pilotti (Sep 02 2022 at 03:25):

Thank you!

Eric Wieser (Sep 02 2022 at 20:26):

Doesn't this exist as docs#lift_list?

Eric Wieser (Sep 02 2022 at 20:27):

You need to write the ↑ explicitly though


Last updated: Dec 20 2023 at 11:08 UTC