Stream: MetaCoq

Topic: Difference between existential variables and metavariables


view this post on Zulip Jakob Botsch Nielsen (Jul 31 2020 at 11:19):

What is the difference between evars and metavars that both appear in Coq's kernel AST? I see that MetaCoq has only the evar constructor.

view this post on Zulip Théo Winterhalter (Jul 31 2020 at 11:58):

I'm not an expert but I think meta variables are used for unification for the old apply, but now pretty much everything else uses evars. Someone with better knowledge will probably give you more insight though.

view this post on Zulip Enrico Tassi (Jul 31 2020 at 12:59):

The Meta term constructor is a relict of the past, used by legacy unification. It's morally an evar but since it lacks the local substitution (the scope) and a type in the evar map... it is not very sound

view this post on Zulip Jakob Botsch Nielsen (Jul 31 2020 at 13:02):

I see, thanks for the responses!


Last updated: Aug 11 2022 at 02:03 UTC