coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: CJ Bell <cbell AT CS.Princeton.EDU>
- To: Jason Gross <jasongross9 AT gmail.com>
- Cc: Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>, Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Export Without Notation
- Date: Fri, 17 May 2013 13:25:04 -0400
On Fri, May 17, 2013 at 12:52 PM, Jason Gross
<jasongross9 AT gmail.com>
wrote:
> Is there a reason that files don't pack notations into scopes specific to
> the development, and then have one module which can be imported for
> notations which just opens the appropriate scopes and binds the appropriate
> scopes to the appropriate types?
Because defining, or even reserving, a notation changes the parsing
behavior regardless of whether the scope is opened or not. If the
notation is defined within a module, then it does not change the
parsing behavior until the module is imported.
For example:
Notation "a ; b" := (plus a b) (at level 50) : my_scope.
(* Records can no longer be parsed, even though my_scope has not been opened!
*)
Record a := {aa:nat; bb:nat}.
In comparison:
Module A.
Notation "a ; b" := (plus a b) (at level 50) : my_scope.
End A.
(* Not broken *)
Record a := {aa:nat; bb:nat}.
Import A.
(* Broken *)
Record b := {cc:nat; dd:nat}.
Defining a notation for ";" is a little contrived because it should
*never* be done, but there are many other ways to define notations
that conflict with each other in this way (even when their scopes are
not open).
-cj
- [Coq-Club] Export Without Notation, Gregory Malecha, 05/17/2013
- Re: [Coq-Club] Export Without Notation, Arnaud Spiwack, 05/17/2013
- Re: [Coq-Club] Export Without Notation, CJ Bell, 05/17/2013
- Re: [Coq-Club] Export Without Notation, Pierre Boutillier, 05/17/2013
- Re: [Coq-Club] Export Without Notation, CJ Bell, 05/17/2013
- Re: [Coq-Club] Export Without Notation, Jason Gross, 05/17/2013
- Re: [Coq-Club] Export Without Notation, CJ Bell, 05/17/2013
- Re: [Coq-Club] Export Without Notation, Pierre Boutillier, 05/17/2013
- Re: [Coq-Club] Export Without Notation, CJ Bell, 05/17/2013
- Re: [Coq-Club] Export Without Notation, Arnaud Spiwack, 05/17/2013
Archive powered by MHonArc 2.6.18.