The Coq mailing list

[CJ Bell <cbell AT CS.Princeton.EDU>]

> Anyway, I see an annoying point : Using notations in the module where you 
> define stuff you
> make notations for asks for defining notations twice. As you can see, 
> notations about
> vectors are defined twice. Once locally in order to be allowed to use [] 
> and :: in
> VectorDef module but not disturb other modules and once in the correct 
> module to make
> them publicly available.

This is true if you want to define the notation inline with an
Inductive, but in your case, I think you could define the notation in
parts, like this:


(* ...defs... *)

Module Internal_ListNotations.
  Notation "[]" := (nil _).
  Notation "h :: t" := (cons _ h _ t) (at level 60, right associativity).
Module Internal_ListNotations.

Import Internal_ListNotations.

(* ...more defs & lemmas... *)

Module VectorNotations.
  Export Internal_ListNotations.
  Notation " [ x ] " := (x :: []) : vector_scope.
  Notation " [ x ; .. ; y ] " := (cons _ x _ .. (cons _ y _ (nil _))
..) : vector_scope.
  Notation "v [@ p ]" := (nth v p) (at level 1, format "v [@ p ]") :
vector_scope.
  Open Scope vector_scope.
End VectorNotations.



However, I'm not sure if this approach is ultimately less ugly because
of the module messiness...

-cj