Jakob Israelsen (Feb 16 2023 at 13:46): Jakob Israelsen (Feb 16 2023 at 13:46):In an effort to better understand how types work in Coq, I wanted to try to make very simple proof synthesis in our extension (if the type of the goal is the same as a lemma, or hypothesis, suggest it).
Currently, I have managed to get the type of the goal as an Evd.econstr, and the types of the hypotheses as Constr.t. As far as I can see, Evd.econstr is a Constr.constr, which is a constr.t. However, ecd.mli does not expose this, and I can therefore not figure out how to compare the type of the goal with the type of a hypothesis. Any idea how to do this?
Gaëtan Gilbert (Feb 16 2023 at 13:52):Evd.econstr is also called EConstr.t and the basic functions to manipulate it are in module EConstr ie econstr.ml(i)
when in a proof context ie if you have an evar map around you should prefer looking up hypotheses as econstr ie using EConstr.lookup_named rather than Environ.lookup_named
Jakob Israelsen (Feb 16 2023 at 14:18):How do you get the goal type in that context? Currently, I am using the Evd.evar_concl which is what returns the Constr.t, but I don't know if there is another function I should be calling to get the goal type?
Gaëtan Gilbert (Feb 16 2023 at 14:34):https://github.com/coq/coq/blob/8e0314415cc3cd528fc81bf11075d294179f880a/engine/evd.mli#L111 returns econstr though?
typically you would do something like
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
something using (EConstr.lookup_named name_of_hyp env)
end
using evar_concl and evar_info is more for low level code
Jakob Israelsen (Feb 16 2023 at 14:40):You're right, it's the hypothesis that is a constr.t, so my earlier message was wrong. I'll try looking into the Proofview.Goal module. Thanks for the help
Last updated: Apr 19 2024 at 10:02 UTC