Bas Spitters
Bas Spitters
M-. jumps to definition. Looking at the behavior of emacs TAGS, I would expect M-* to bring me back. Perhaps one could add such a key-binding?
With 8.6 we seem to have most of the technology to create agda style term construction. [agda manual](http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.QuickGuideToEditingTypeCheckingAndCompilingAgdaCode) I thought I'd record it here. @gares may also have insights into...
@amahboubi rightly observed in #401 that this deserves it's own issue. We are currently considering whether it is feasible to integrate elliptic https://github.com/strub/elliptic-curves-ssr and fiat-crypto. So far things look positive....
It would be great to move these tips to a more central place. @zimmi48 is doing great work organizing these things.
This can be done as in the https://github.com/HoTT/HoTT @Zimmi48 , does the coq-community has standard template for this? It makes sense to role out this tools uniformly
LaTeX ?
This looks excellent. Did you consider supporting latex? Perhaps via RTF.
https://hott.github.io/HoTT/dep-graphs/
jscoq was [designed](https://arxiv.org/pdf/1701.07125) with literate programming in mind. Literature programming also motivated book.py / book.v We now have the beautiful jshott. However, the two ideas were never combined. @ejgallego would...
It would be nice to have Program for HoTT, e.g. for use in HoTT-Classes. I keep on forgetting what we have done already. There was a discussion here: https://github.com/HoTT/HoTT/commit/6a99db1c31fe267fdef7be755fa169fb6a87e3cf However,...