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.
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.
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
I see, thanks for the responses!
Last updated: Aug 11 2022 at 02:03 UTC