# Notation for a coinductive type

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

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

and I can construct its objects without error:

``````(* 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:

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

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

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,

``````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), but the term you would bind it too (`cofix Foo : ilist := Foo`) is not valid because it is not guarded.