# Overload list notation

**URL:** <https://discourse.rocq-prover.org/t/overload-list-notation/1450>\
**Category:** Using Rocq\
**Tags:** notation\
**Created:** [September 24, 2021, 12:04pm UTC](https://discourse.rocq-prover.org/t/overload-list-notation/1450 "2021-09-24T12:04:47Z")\
**Posts on this page:** 4\
**Page:** 1

<div class="post-metadata">

**Author:** ![pjm](https://avatars.discourse-cdn.com/v4/letter/p/c6cbf5/32.png) [@pjm](https://discourse.rocq-prover.org/u/pjm)\
**Post date:** [September 24, 2021, 12:04pm UTC](https://discourse.rocq-prover.org/t/overload-list-notation/1450/1 "2021-09-24T12:04:47Z")

</div>

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

```auto
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?

---

<div class="post-metadata">

**Author:** ![herbelin](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/herbelin/32/111_2.png) [@herbelin](https://discourse.rocq-prover.org/u/herbelin)\
**Post date:** [September 25, 2021, 9:15am UTC](https://discourse.rocq-prover.org/t/overload-list-notation/1450/2 "2021-09-25T09:15:17Z")

</div>

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

```auto
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!

---

<div class="post-metadata">

**Author:** ![pjm](https://avatars.discourse-cdn.com/v4/letter/p/c6cbf5/32.png) [@pjm](https://discourse.rocq-prover.org/u/pjm)\
**Post date:** [September 27, 2021, 11:37am UTC](https://discourse.rocq-prover.org/t/overload-list-notation/1450/3 "2021-09-27T11:37:45Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![herbelin](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/herbelin/32/111_2.png) [@herbelin](https://discourse.rocq-prover.org/u/herbelin)\
**Post date:** [September 27, 2021, 4:23pm UTC](https://discourse.rocq-prover.org/t/overload-list-notation/1450/4 "2021-09-27T16:23:02Z")

</div>

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