Janno (Jun 30 2020 at 11:32): 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..)
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
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
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
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.
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?
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.
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)
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: Jun 05 2023 at 09:01 UTC