Coq-Equations
Coq-Equations copied to clipboard
mattam82
Emacs support?
Hi, I just read about Equations and love it so much.
To my understanding, I find that it greatly resembles style from Agda. However, I personally find one strength from Agda is its Emacs interaction. Hence I am wondering whether it's possible to have similar form of interaction for Equations as well? If dependent type programs get more complex, it can be challenging to fill in all terms in one shot.
Or do you have some tricks when you write dependent programs using Equations yourself?
I don’t have many tricks, indeed Emacs support is lacking. One can use _ to not give a term directly and then try to figure out which obligation corresponds to which hole to gather what type is needed. I have little emacs-fu so I’d need someone knowledgeable to help implement things. Le dim. 23 sept. 2018 à 14:55, Jason Hu [email protected] a écrit :
Hi, I just read about Equations and love it so much.
To my understanding, I find that it greatly resembles style from Agda. However, I personally find one strength from Agda is its Emacs interaction. Hence I am wondering whether it's possible to have similar form of interaction for Equations as well? If dependent type programs get more complex, it can be challenging to fill in all terms in one shot.
Or do you have some tricks when you write dependent programs using Equations yourself?
— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/mattam82/Coq-Equations/issues/135, or mute the thread https://github.com/notifications/unsubscribe-auth/AAGARTUxTRi3g_P9IzeEbGSCkFQQOBsMks5ud9ktgaJpZM4W11DF .
In the current master branch, one can use Equations? foo to get goals instead of obligations corresponding to the holes of the program. This ressembles Agda-style interaction a little bit better. One would need some GUI API though to support displaying what is the type of the hole at hand. @cpitclaudel @ejgallego would you have an idea how easy it would be to implement something like this?
that's very great. let me try it out later. I am wondering though, if i have more than one holes, how should I correspond the goals to holes? are the holes indexed?
Most of the time, it follows textual order, but not always. It's only a poor man's solution :)
It should be possible to do better, indeed; I don't really know what the API would look like. Currently you can ask for the goal in a particular state of the STM, but not at a particular position in the buffer. If we generalized the API to allow asking "what goal should I display here", then it would smoothly handle this use case, I imagine.
