I have defined a type for non-empty lists and some notations to be able to build them like standard lists.

From Coq Require Import List.
Import ListNotations.
Inductive nlist (A : Type) : Type :=
| nsing : A -> nlist A
| ncons : A -> nlist A -> nlist A.
Declare Scope nlist_scope.
Delimit Scope nlist_scope with nlist.
Notation "[ x ]" := (nsing _ x) : nlist_scope.
Notation "[ x ; .. ; y ; z ]" := (ncons _ x (.. (ncons _ y (nsing _ z)) ..)) : nlist_scope.
Check [1]%nlist. (* : nlist nat *)
Check [1]. (* : list nat *)
Check [1;2]%nlist. (* : nlist nat *)
Fail Check [1;2]. (* Unknown interpretation for notation "[ _ ; .. ; _ ; _ ]". *)

My notation seems to break the standard list ones but I cannot understand why. Is it the intended behavior? How can I make my definitions working correctly?

Hi, it is because the standard notation for lists (in file List.v) is defined by:

Notation "[ ]" := nil (format "[ ]") : list_scope.
Notation "[ x ]" := (cons x nil) : list_scope.
Notation "[ x ; y ; .. ; z ]" := (cons x (cons y .. (cons z nil) ..)) : list_scope.

i.e. with a special case for singleton lists. The parser is unfortunately not smart enough to recognize that both styles are equivalent, so, you would have to explicitly have a special case for singleton in your notation for nlist too!

Thank you for taking the time to answer my question. However I still donâ€™t understand what in my example breaks the standard list notation. I have defined the singleton case as you suggested: the notation for nlist indeed work with an arbitrary number of elements, but then I cannot use [_;_] for regular lists anymore, even if the nlist scope is not open.

Sorry, I spoke much too quickly. The conflict between both notations is for the recursive part [ x ; y ; .. ; z ] vs [ x ; .. ; y ; z ]. Both forms have the same parsing rule (*) but a different internal recursive pattern. This means there is â€śconceptualâ€ť bug in identifying the parsing rules but not the internal recursive pattern. Somehow, it is the scope which should decide which recursive pattern to use. This is worth a bug report. Thanks for the interesting example.

(*) The parsing rule for [ x ; .. ; y ; z ] is internally modified to [ x ; y ; .. ; z ], i.e. "["; term LEVEL "200"; ";"; LIST1 (term LEVEL "200") SEP ";"; "]" when shown with Print Grammar constr (**), because otherwise, after having grabbed as many ; y as possible, one would never find a final ; z.

(**) Actually even further to "["; term LEVEL "200"; ";"; term LEVEL "200"; ";"; LIST1 (term LEVEL "200") SEP ";"; "]" to increase the factorization with potential non-recursive notations starting with "[ x ; y"