# Overload list notation

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"`

1 Like