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 ?
All ideas are welcome
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).
I see, thanks for pointing me to this feature ! we’ll try it and probably report some things on it