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 %nlist. (* : nlist nat *) Check . (* : 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?