coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jasper Stein <J.Stein AT cs.ru.nl>
- To: roconnor AT theorem.ca
- Cc: Coq Club <coq-club AT pauillac.inria.fr>
- Subject: Re: [Coq-Club] Notiations inside Sections.
- Date: Mon, 21 Mar 2005 12:07:56 +0000
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Op zaterdag 19 maart 2005 10:28, schreef
roconnor AT theorem.ca:
> I am creating a file, but I don't want to export every definition and
> lemma. So I create a Section and use Let and Remark on the items I don't
> want to export. But I also want to define some Notations. The Notations
> don't seems to survive pas the end of my Section.
>
> Is there a simple solution to my problem?
The obvious (but not so elegant) solution is to re-declare your Notations
after ending the section.
Section concat.
Definition concat:=...
Notation "a ++ b" := concat a b.
End concat.
Notation "a ++ b" := concat a b.
Jasper
--
The problem with having an open mind is that people toss in garbage
- [Coq-Club] Notiations inside Sections., roconnor
- Re: [Coq-Club] Notiations inside Sections., Jasper Stein
- Re: [Coq-Club] Notiations inside Sections., Hugo Herbelin
- Re: [Coq-Club] Notiations inside Sections., Jasper Stein
Archive powered by MhonArc 2.6.16.