coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jason Gross <jasongross9 AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: [Coq-Club] Printing the scopes of notations
- Date: Tue, 29 Jul 2014 16:30:40 +0100
Hi,
Is it possible to get Coq to tell me what scopes are bound in notations? For example, if I do
Notation "~ x" := (not x%bool).
I'd like Coq to tell me that [x] is in bool_scope.
Thanks,
Jason
- [Coq-Club] Printing the scopes of notations, Jason Gross, 07/29/2014
Archive powered by MHonArc 2.6.18.