Notation for a coinductive type

Using Coq
1

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?

2

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.