coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] yet another pb with Notation (from Init/Logic.v)

From: Hugo Herbelin <Hugo.Herbelin AT inria.fr>
To: Benjamin Pierce <bcpierce AT cis.upenn.edu>
Cc: Arthur Chargu�raud <arthur.chargueraud AT inria.fr>, coq-club AT inria.fr
Subject: Re: [Coq-Club] yet another pb with Notation (from Init/Logic.v)
Date: Sun, 16 May 2010 15:23:29 +0200

Hi,

> An alternative that we're just beginning to look at seriously is
> using unicode notations, but we're not completely sure that the
> world is ready for this...

For writing, both the emacs "tex" input method for proof-general and
the uim input methods for coqide (Unix) work apparently well.

Otherwise, I remember that the caml revised syntax implemented by
camlp5 (and re-used by G�rard Huet with name Pidgin ML for didactic
purpose) proposes the following for sequences (adapted to Coq):

Notation "'do' { e1 ; e2 ; .. ; en }" :=
(CSeq .. (CSeq e1 e2) .. en) (at level 0).

(see http://cristal.inria.fr/~ddr/camlp5/doc/html/revsynt.html)

Hugo

[Coq-Club] record field is "lost" if import is used, Patrice Chalin
- Re: [Coq-Club] record field is "lost" if import is used, Hugo Herbelin
  - [Coq-Club] yet another pb with Notation (from Init/Logic.v), Jean-Francois Monin
    - Re: [Coq-Club] yet another pb with Notation (from Init/Logic.v), Hugo Herbelin
      - Re: [Coq-Club] yet another pb with Notation (from Init/Logic.v), Dan Colish
      - Re: [Coq-Club] yet another pb with Notation (from Init/Logic.v), Benjamin Pierce
        
        Re: [Coq-Club] yet another pb with Notation (from Init/Logic.v), Arthur Chargu�raud
        
        Re: [Coq-Club] yet another pb with Notation (from Init/Logic.v), Benjamin Pierce
        
        Re: [Coq-Club] yet another pb with Notation (from Init/Logic.v), Hugo Herbelin