The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

I usually go with your option #1 and as you mentioned it is not perfect.

I would be great to have "Global" modifier for "Notation" command like we have for 

"Instance".

Vadim

--

CMU ECE PhD candidate

Mobile: +1(510)220-1060

On Tue, Nov 22, 2016 at 4:13 PM, Valentin Robert <valentin.robert.42 AT gmail.com> wrote:

Dear club,

According to the reference manual:

"Notations do not survive the end of sections."

I would like to understand whether a) this is a wanted feature b) this is a constraint or c) a choice of the current implementation, or d) this is due to some theoretical issue with trying to make them survive.

In particular, I often find myself in the following conundrum:

- I open a section and define some section context (variables and definitions).

- I define something that I'd like to use a notation for.

- I want to use the notation within the rest of the section, but also outside the section.

It seems my options are:

i)

Define the notation once for within the section, and then again after leaving the section.

Not great if I later decide to change the notation and want to keeps things uniform.

ii)

Abandon the idea of having the notation within the section.

Makes the section theorems harder to read from the source code point of view.

iii)

Close the section. Define the notation. Open a similar section.

Not great if the section setup is heavy, and this artificially breaks sections into weird notation-separated-blocks.

Is there a better way of going about this I'm missing? Otherwise, which poison do people pick?

- Valentin