Hi !
In order to avoid getting noise from user defined notations, I’d like to know if there is a way at the moment to ask Coq to display a fully rewritten vernac command, unrolling all notations. Just to be clear, I don’t want the result of the command to be displayed without notation (there are Print commands for that), but the command itself.
For example, If I input Print (3 + 4)., I’d like to get Print (plus (S (S (S O))) (S (S (S (S 0)))). as a result.
I don’t know if this already exists. If it is not the case, what would be the best way to achieve that ? A Coq plugin ? Extracting the Notation mechanism in a third-party tool ?
You can use the -beautify option to get Coq to reprint what it parses. The output is not always so “beautiful” and can even be a bit buggy because it is not much tested, but it can get you quite close to what you’re asking (and feel free to open issues about it).
For instance, if I write a test.v file with the following content:
Unset Printing Notations.
Check (3 + 4).
then I run coqc -beautify test.v, it creates a new file called test.v.beautified which contains:
Unset Printing Notations.Check Nat.add (S (S (S
O))) (S (S (S (S O)))).
So, while the spacing is incorrectly reproduced (and would deserve an issue to be opened about this), the result is pretty much what you asked for (the Print command from your example doesn’t exist).
