coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Pierre Courtieu <pierre.courtieu AT gmail.com>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] How to look up notation definitions?
- Date: Thu, 31 Jul 2014 13:42:47 +0200
You can use [ Locate "{" ] for example to see all notations involving
a curly bracket.
Or [ Locate "_ + _" ].
As Cédric said you can just set the "Printing All" switch ON (Set
Printing All) by using menus of coqide or proofgeneral (Coq -> OTHER
QUERIES -> Print ith goal (show all), shortcut to be bound to
(coq-Show-with-implicits), by default C-u C-c C-a C-s).
Best regards,
Pierre
2014-07-31 10:16 GMT+02:00 Cedric Auger
<sedrikov AT gmail.com>:
>
>
> 2014-07-31 9:30 GMT+02:00
> <michael.soegtrop AT intel.com>:
>
>> Dear Coq users,
>>
>> is there a good way to look up the definition of a notation or to unfold
>> notations in a goal or hypothesis? In proofs one typically has to use the
>> "real names", but I tend to forget these and the best way I found to look
>> up
>> the definition of a notation is grep, which is not so convenient.
>>
>> Best regards,
>>
>> Michael
>
>
> You can deactivate notations (in the menus of the IDE), read your
> hypothesis, and reactivate them.
> That would not qualify as a "good way" since it will unfold *all* the
> notations and not only the one you want.
> Still, it seems better than using grep (although the purpose is slightly
> different as with my solution you need to have an hypothesis under focus in
> your IDE, and you have the advantage of not manually apply the Notation,
> while in the grep solution, you get the definition and do not require to
> have an hypothesis under focus, which can be helpful if you want to write a
> term or just to focus on the Notation itself, but you have to manually apply
> the Notation to your context if you have one).
>
> I think there is something that does what your grep tool does. That must be
> in the reference manual (Locate).
>
> http://coq.inria.fr/refman/Reference-Manual008.html#hevea_command135
>
>
> By the way, the documentation has problems with the '%' character as seen
> in:
>
> http://coq.inria.fr/refman/Reference-Manual008.html#hevea_command132
>
>
>
> --
> .../Sedrikov\...
- [Coq-Club] How to look up notation definitions?, michael.soegtrop, 07/31/2014
- Re: [Coq-Club] How to look up notation definitions?, Christopher Ernest Sally, 07/31/2014
- Re: [Coq-Club] How to look up notation definitions?, Cedric Auger, 07/31/2014
- Re: [Coq-Club] How to look up notation definitions?, Pierre Courtieu, 07/31/2014
- RE: [Coq-Club] How to look up notation definitions?, Soegtrop, Michael, 07/31/2014
- Re: [Coq-Club] How to look up notation definitions?, Pierre Courtieu, 07/31/2014
Archive powered by MHonArc 2.6.18.