coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Michael Shulman <shulman AT sandiego.edu>
- To: Coq Club <coq-club AT inria.fr>
- Subject: [Coq-Club] displaying the level of a notation
- Date: Wed, 18 Nov 2015 09:14:22 -0800
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=viritrilbia AT gmail.com; spf=Pass smtp.mailfrom=viritrilbia AT gmail.com; spf=None smtp.helo=postmaster AT mail-lb0-f173.google.com
- Ironport-phdr: 9a23:zyAWEReyx3M+W7Nnx9mX3Uy7lGMj4u6mDksu8pMizoh2WeGdxc69Zh7h7PlgxGXEQZ/co6odzbGG7ua+ACdRut6oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLDvvcOKKFQTzBOGIppMbzyO5T3LsccXhYYwYo0Q8TDu5kVyRuJN2GlzLkiSlRuvru25/Zpk7jgC86l5r50IeezAcq85Vb1VCig9eyBwvZWz9EqLcQzazXwFGk4SjxAAVwPC9VTxWor7mir8rOt0nieAa57YV7cxDBGj5KdiRRugsycaMzsw9imDkcxtiKdSpjq6rhpzwoPbZ8eYOOcoLfCVRs8TWWcUBpUZbCdGGI7pKtJXV+c=
Is there a command to display the level of a particular notation?
"Locate" shows what a notation is defined to mean, but not its level.
So far the only ways I have found to figure out the level of a
notation are to try to track down the source file where the notation
was declared, or to "Print Grammar constr" and search through the (not
very user-friendly) output for the notation in question.
Mike
- [Coq-Club] displaying the level of a notation, Michael Shulman, 11/18/2015
- Re: [Coq-Club] displaying the level of a notation, Hugo Herbelin, 11/20/2015
Archive powered by MHonArc 2.6.18.