Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] On the persistence of notations across and beyond sections

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] On the persistence of notations across and beyond sections


Chronological Thread 
  • From: Andreas Abel <andreas.abel AT ifi.lmu.de>
  • To: Valentin Robert <valentin.robert.42 AT gmail.com>, "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] On the persistence of notations across and beyond sections
  • Date: Thu, 24 Nov 2016 17:37:25 +0100
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=andreas.abel AT ifi.lmu.de; spf=None smtp.mailfrom=andreas.abel AT ifi.lmu.de; spf=None smtp.helo=postmaster AT acheron.ifi.lmu.de
  • Ironport-phdr: 9a23:PrFjNh97NaXZHf9uRHKM819IXTAuvvDOBiVQ1KB91ewcTK2v8tzYMVDF4r011RmSDN6dsaMP27qe8/i5HzdfsdDZ6DFKWacPfiFGoP1epxYnDs+BBB+zB9/RRAt+Iv5/UkR49WqwK0lfFZW2TVTTpnqv8WxaQU2nZkJdb974EY/Kjsmxy/v6u9iKO10J13KBZuZMJRG7qxnQsIEshoFvMLp5ngXApnZOZ+VQg3lvL1+Jg1CgvO+/+Zdi92JbvPd3s4YKWqLjOq88ULZwDTI8Mmlz6teh/U3IShLK7X8BWE0XlABJCk7L9kepcI32t37TsOZn1SCBdeT8QLR8DT2k471mQQSugS0KMxY4/mCRjsltyq5W9kHy7ydjypLZNdnGfMF1ebnQKJZDHTJM

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/



Archive powered by MHonArc 2.6.18.

Top of Page