Stream: Coq devs & plugin devs

Topic: Instantiating Evars


view this post on Zulip Janno (Jun 30 2020 at 11:32):

Is there a function like Evd.define that also checks that the instantiation is not cyclic? It seems I can use define to instantiate an evar with itself which (I think) is illegal (and certainly leads term printing into an endless loop..)

view this post on Zulip Matthieu Sozeau (Jun 30 2020 at 12:03):

Evarsolve.evar_define is what you're looking. for. Evd.define is quite low-level indeed and does no such checks

view this post on Zulip Janno (Jun 30 2020 at 12:14):

Great, thank you! I also see instantiate_evar in that file but I can't tell from the description what the differences are. Will evar_define not unify the types? That's something that I would like to avoid paying for since I know the types are convertible

view this post on Zulip Emilio Jesús Gallego Arias (Jun 30 2020 at 14:05):

Adding some docstrings to the mli files would be great if you got a couple of minutes

view this post on Zulip Janno (Jun 30 2020 at 17:43):

Adding some docstrings to the mli files would be great if you got a couple of minutes

If that was meant for me then I think I first need to understand any of it before I start documenting these functions.

view this post on Zulip Janno (Jun 30 2020 at 17:44):

It seems that evar_define removes casts from the solution—at least when it's given Evarconv.evar_unify as a unifier. Is there a way around that?

view this post on Zulip Janno (Jun 30 2020 at 17:50):

I suppose I'll copy what Refiner.refine does: check that the evar doesn't appear in the solution and then call Evd.define.

view this post on Zulip Janno (Jul 01 2020 at 07:06):

For the benefit of anyone else who'd like to instantiate evars without calling unification: it's very likely that the approach above is wrong except for goal evars (I don't understand the reason but it's something to do with the identity substitution)

view this post on Zulip Beta Ziliani (Jul 04 2020 at 14:45):

I missed this thread. Sorry!
It's ok to not unify the types if you know that the evar and what you're instantiating it with have the same type. What is incorrect is to not do the inverse of the substitution.


Last updated: Oct 16 2021 at 09:07 UTC