coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Christopher Ernest Sally <christopherernestsally 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 16:01:16 +0800

Dear Michael

will "Print <notation>." serve?

Best

Chris

On 31 July 2014 15:30, <michael.soegtrop AT intel.com> wrote:

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

[Coq-Club] How to look up notation definitions?, michael.soegtrop, 07/31/2014
- Re: [Coq-Club] How to look up notation definitions?, Pierre-Evariste Dagand, 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