# Evaluating Notations on input commands

**URL:** <https://discourse.rocq-prover.org/t/evaluating-notations-on-input-commands/642>\
**Category:** Using Rocq\
**Created:** [February 26, 2020, 8:14am UTC](https://discourse.rocq-prover.org/t/evaluating-notations-on-input-commands/642 "2020-02-26T08:14:13Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![vsiles](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/vsiles/32/274_2.png) [@vsiles](https://discourse.rocq-prover.org/u/vsiles)\
**Post date:** [February 26, 2020, 8:14am UTC](https://discourse.rocq-prover.org/t/evaluating-notations-on-input-commands/642/1 "2020-02-26T08:14:13Z")

</div>

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 ?

All ideas are welcome 😃  
Best,  
V.

---

<div class="post-metadata">

**Author:** ![Zimmi48](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/zimmi48/32/7_2.png) [@Zimmi48](https://discourse.rocq-prover.org/u/Zimmi48)\
**Post date:** [February 26, 2020, 1:41pm UTC](https://discourse.rocq-prover.org/t/evaluating-notations-on-input-commands/642/2 "2020-02-26T13:41:18Z")

</div>

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:

```coq
Unset Printing Notations.
Check (3 + 4).

```

then I run `coqc -beautify test.v`, it creates a new file called `test.v.beautified` which contains:

```coq
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).

---

<div class="post-metadata">

**Author:** ![vsiles](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/vsiles/32/274_2.png) [@vsiles](https://discourse.rocq-prover.org/u/vsiles)\
**Post date:** [February 26, 2020, 1:58pm UTC](https://discourse.rocq-prover.org/t/evaluating-notations-on-input-commands/642/3 "2020-02-26T13:58:50Z")

</div>

I see, thanks for pointing me to this feature ! we’ll try it and probably report some things on it 😃