The Coq mailing list

[Pierre Casteran <casteran AT labri.fr>]

It seems that some problems come from the "?"

For instance,
This is OK :

Grammar mytypes int_chevrons :=
    chevrons [ ">>"] -> [(nil nat)].

But not this one.

Grammar mytypes2 int_chevrons2 :=
    chevrons2 [ ">>"] -> [(nil ?)].

Toplevel input, characters 136-137
> Grammar mytypes2 int_chevrons2 :=     chevrons2 [ ">>"] -> [(nil ?)].
>                                                                  ^
Syntax error: [Prim.ast] expected after [astident] (in [Prim.ast])

Pierre

Any way, is the notation for polymorphic lists is to be available,
it will be OK.

Pierre



Hugo Herbelin wrote:
>   Hi,
>  
>
> >  I wanted to have some notation for some kinds of lists.
> > What is wrong with the following definition ?
> > Pierre
> >
> > Require PolyList.
> >
> > Grammar listes inside_list : ast list :=
> >   inside_cons  [constr($a)  listes:inside_list($b)] ->
> >                 [(cons $a $b)]
> >
> > |inside_one  [constr0($a) ">>"] ->[(cons $a (nil ?))].
> >
> >
> > Syntax error: [Prim.ast] expected after [astident] (in [Prim.ast])
>
>
>   The type "ast list" implies that the right hand side is parsed as an
> ast list, but you give a term. Use ": constr" instead.
>
>
>   I seize to opportunity to question the relevance of continuing
> supporting Grammar (for constr) in the next versions of Coq knowing
> that a new mechanism for symbolic notations has been developed. The
> new mechanism allows to define e.g. the concrete syntax for sig (both
> parsing and printing) as simply as follows:
>
> Notation "{ x : A | P }" := (sig A [x:A]P)   (at level 1).
>
>   The new mechanism allows also to use the concrete syntax of operators
> on Z or R (or even nat or positive) without quotes or double quotes
> (one just says in advance what should be the default interpretation of
> symbols in the current development).
>
>   However it does not support recursive notations and hence does not
> allow to write a list in a format like << a b c >> or {a;b;c;d}, etc.
>
>   Hugo
>
>   



--
Pierre Casteran,
LaBRI, Universite Bordeaux-I      |
351 Cours de la Liberation        |
F-33405 TALENCE Cedex             |
France                            |
tel : (+ 33) 5 56 84 69 31
fax : (+ 33) 5 56 84 66 69
email: Pierre . Casteran @ labri . u-bordeaux . fr  (but whithout white 
space)
www: http://dept-info.labri.u-bordeaux.fr/~casteran