You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
This is a bit trickier to fix. It's not limited to meta-functions, but meta-functions are corner case.
In your example you want an arrow coercion to take place inside a map. The difficulty is that the type mismatch is not local to the term x |--> allocate(v), which is a valid term. The mismatch appears between the term x |--> allocate(v) and E and so you need an arrow coercion Map(String, allocate__meta) --> Map(String, V).
In this particular example the correct outcome is to eagerly reduce all meta-functions which are not explicitly reduced.
I think the editor behavior is correct for the the general case when allocate(v) is not a meta-function.
This is not a case of a coercion. Applications of meta-functions need to be lifted out of term construction in general. This is a different transformation.
Meta-function is not lifted from map construction in following rule:
The text was updated successfully, but these errors were encountered: