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..)
Evarsolve.evar_define
is what you're looking. for. Evd.define
is quite low-level indeed and does no such checks
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
Adding some docstrings to the mli files would be great if you got a couple of minutes
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.
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?
I suppose I'll copy what Refiner.refine
does: check that the evar doesn't appear in the solution and then call Evd.define
.
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)
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