coq-tricks
coq-tricks copied to clipboard
tchajed
Tricks you wish the Coq manual told you
I found the `exploit` tactic useful in case where I have `H : P -> Q` in the context or as a lemma and would like to have `Q` in...
The only thing blocking this is that some examples demo coq master features, and these shouldn't be run on older versions. We can probably somehow set this up (without branches),...
The [convoy pattern](http://adam.chlipala.net/cpdt/html/MoreDep.html) is invaluable for writing functions over dependent types. It would be nice to have a good example of it here too.
It would be great to move these tips to a more central place. @zimmi48 is doing great work organizing these things.
By activating GitHub Pages, this repo can now deploy documentation for every new commit that would live at https://coq-community.org/coq-tricks There are two kinds of documentation that I think can be...
Suppose we have something like ```Coq (* file_1.v*) Module A. Inductive Ind_1 : Set := | TERM_1 | TERM_2 . End A. ``` And we want to import this module...
We should change references to the old `coq-community/coq-tricks` URL to account for the Rocq renaming, as well as fixing the README and some other places in the opam file.
