The Coq mailing list

[Pierre Casteran <casteran AT labri.fr>]

Hi !

I plan to build a project in Computationnal linguistics on Coq.
It is important I can read/print sentences in another way than
binary cons-trees !


Pierre


>   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