coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Perce Strop <percestrop AT outlook.com>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: RE: [Coq-Club] How to use Notations inside of Modules?
- Date: Thu, 25 Dec 2014 16:02:56 +0000
- Importance: Normal
Hi,
You can use the command "Import int32" to use your notation. If you don't want to import everything, you should put your notation in an isolated module.
Perce
You can use the command "Import int32" to use your notation. If you don't want to import everything, you should put your notation in an isolated module.
Perce
- [Coq-Club] How to use Notations inside of Modules?, Chris Dams, 12/25/2014
- RE: [Coq-Club] How to use Notations inside of Modules?, Perce Strop, 12/25/2014
- Re: [Coq-Club] How to use Notations inside of Modules?, Chris Dams, 12/28/2014
- RE: [Coq-Club] How to use Notations inside of Modules?, Perce Strop, 12/28/2014
- Re: [Coq-Club] How to use Notations inside of Modules?, Chris Dams, 12/29/2014
- RE: [Coq-Club] How to use Notations inside of Modules?, Perce Strop, 12/28/2014
- Re: [Coq-Club] How to use Notations inside of Modules?, Chris Dams, 12/28/2014
- RE: [Coq-Club] How to use Notations inside of Modules?, Perce Strop, 12/25/2014
Archive powered by MHonArc 2.6.18.