Jakob Botsch Nielsen (Jul 31 2020 at 11:19): 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.
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.
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
Jakob Botsch Nielsen (Jul 31 2020 at 13:02):I see, thanks for the responses!
Last updated: Dec 07 2023 at 14:02 UTC