Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] How to look up notation definitions?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How to look up notation definitions?


Chronological Thread 
  • 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\...



Archive powered by MHonArc 2.6.18.

Top of Page