# Notation for a coinductive type

**URL:** <https://discourse.rocq-prover.org/t/notation-for-a-coinductive-type/1468>\
**Category:** Using Rocq\
**Tags:** notation\
**Created:** [October 22, 2021, 5:06am UTC](https://discourse.rocq-prover.org/t/notation-for-a-coinductive-type/1468 "2021-10-22T05:06:22Z")\
**Posts on this page:** 2\
**Page:** 1

<div class="post-metadata">

**Author:** ![famubu](https://avatars.discourse-cdn.com/v4/letter/f/b19c9b/32.png) [@famubu](https://discourse.rocq-prover.org/u/famubu)\
**Post date:** [October 22, 2021, 5:06am UTC](https://discourse.rocq-prover.org/t/notation-for-a-coinductive-type/1468/1 "2021-10-22T05:06:22Z")

</div>

I made something like a list that keeps repeating using `CoInductive` with

```auto
CoInductive ilist {A : Type} : Type :=
| icons : A -> ilist -> ilist.

```

and I can construct its objects without error:

```auto
(* Means a list like [[3;4; 3;4; 3;4; 3;4; .....]] *)
CoFixpoint foo := (icons 3 (icons 4 foo)).

```

How can we make a notation to do the list construction?

I was trying to make a notation that will allow constructing the same list as above as: `[[3; 4; NIL]]`.

Where `NIL` is used to denote the end of the ‘basic part’ (ie, the part which keeps repeating in the list) of the list.

So I tried:

```auto
Notation "[[x ; y ; .. ; z ; 'NIL']]" := (cofix Foo : ilist :=
  (icons x (icons y .. (icons z Foo) .. )))

```

That ran okay.

But using the notation itself didn’t work.

```auto
Compute [[NIL]].
(*
Syntax error: ';' expected after [term level 200] (in [term]).
 *)

Compute [[1 ; 2 ; 3 ; NIL]].
(* 
Syntax error: ';' or ';' 'NIL' ']]' expected (in [term]).
 *)

```

What am I missing here?

---

<div class="post-metadata">

**Author:** ![MevenBertrand](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/mevenbertrand/32/555_2.png) [@MevenBertrand](https://discourse.rocq-prover.org/u/MevenBertrand)\
**Post date:** [November 4, 2021, 1:24pm UTC](https://discourse.rocq-prover.org/t/notation-for-a-coinductive-type/1468/2 "2021-11-04T13:24:55Z")

</div>

Not sure what the issue is with the notation you want (I am not a notation expert), but if this is good enough for you,

```auto
Notation "[[x ; .. ; z]]" := (cofix Foo : ilist :=
    (icons x .. (icons z Foo) .. )).

```

should fix your second example. As for the first one, you could add a specific notation (as is done e.g. [for the empty list](https://coq.inria.fr/distrib/current/stdlib/Coq.Lists.List.html#ListNotations)), but the term you would bind it too (`cofix Foo : ilist := Foo`) is not valid because it is not guarded.