The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

  Hi,

> On Tue, 25 Feb 2003, Pierre Corbineau wrote:
> > On Tue, Feb 25, 2003 at 04:38:39PM +0100, Romain Janvier wrote:
> > > I want to write something like that in a tactic:
> > > Tactic Definition tac:=
> > > Match Context With
> > > ...
> > > |[id: (EX ?1| ?2)|-?3] -> Induction id
> > > ...
> >
> > Use the pattern [id: (ex ? ? ?)|-?] instead.
> 
> Along these lines, I've often wanted some way to see the "primitive" form
> of the various notational devices.  Suppose I forget that EX is ex, or
> that ~ is not, or some such; if I wanted to send such a term to Check or
> Print, or use it in a pattern like above, things are very difficult.
> If there could be a command to print a term without using any of the
> special pretty-printing rules, that could be helpful in such a situation.

  In V7.4, the Locate command is applicable to notations:

Coq < Locate "EX _ | _".
"'EX' x | p" := (ex ? [x]p) : core_scope (default interpretation)

  You also have the command "Print Scope core_scope" to see the list
of all standard notations.

Coq < Print Scope core_scope.
Scope core_scope
No delimiters
"( x , y )" := (pair ? ? x y)
"< A , B > ( x , y )" := (pair A B x y)
"< A , B > 'Fst' ( p )" := (fst A B p)
"< A , B > 'Snd' ( p )" := (snd A B p)
"< P , Q > { p , q }" := (conj P Q p q)
etc.

  These commands refer to "scopes" which is an experimental notion
allowing a weak form of overloading.  This is why they are still not
documented.

  Hugo Herbelin