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"