The Coq mailing list

[Andreas Abel <andreas.abel AT ifi.lmu.de>]

Agda has not solved the "notation-outside section" problem either, see

  https://github.com/agda/agda/issues/632

On 23.11.2016 21:46, Hugo Herbelin wrote:
> Dear Valentin,
>
> > 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.
>
> One certainly would like notations to sometimes survive section. If I
> did not implement it, it is because I did not see what clear strategy
> to follow in adapting the notations to the new expression it refers
> to. Thinking to it again now, one could use the strategy that all
> extra arguments of the constants involved in the notation are replaced
> by "_". For instance, that would be fine for an example such as:
>
> Section projection.
>   Variables A B : Type.
>   Definition fst `((x,y):A*B) := x.
>   Notation "p .1" := (fst p).
> End projection.
> (* One would redefine the notation to
> Notation "p .1" := (fst _ _ p).
> *)
>
> But, then, is it reasonable to do that systematically without even
> checking that the added "_" are inferable? Shall we then couple this
> generalization with a test that the arguments are inferable? Or with a
> test that the arguments are declared as implicit? Or really let it
> entirely to the responsability of the user that the resulting notation
> makes sense?
>
> It is this kind of questions that I was not able to answer and which
> led me to not let notations survive sections.
>
> But you're completely right, one could do better, and we can discuss
> further if you are interested.
>
> Hugo


--
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel AT gu.se
http://www2.tcs.ifi.lmu.de/~abel/