Open Alizter opened 1 year ago
Can you provide a couple of examples in the form of Coq code + UI action on it?
It is not clear for me what coq-lsp should do here.
Given
Axiom A : Type.
Axiom B : A -> Type.
Axiom foo : forall (x : A) (y : B x), nat.
if I write foo _ y
then the _
is inferred by Coq. We should be able to hover the mouse over that _
and see A
.
Thanks, so indeed we want to run full elaboration here.
That's actually quite tricky to do properly in Coq as elaboration runs on kernel terms, which don't have any kind of location !
Maxime was interested in improving this API, I did some tries with Hugo too for the coq-layout-engine project, but overall, that still remain tricky.
Actually maybe not everything is lost tho, Coq has support to track location info on holes even when they are converted to evars, but I'm unsure that has been really tested, but indeed, restricting this feature from Ast to Ast mapping to lookup in a hole list could maybe work (tho I bet it will require API changes upstream as to have a loc to evar reverse map)
Like we have hover for identifiers, it would be great to have hover for holes. OCaml already has something similar (maybe even a custom protocol). This would also tie in with the holes based programming idea.