Hi.

I was trying to make a notation that would let me create instances of an infinite list made as a CoInductive type.

```
CoInductive ilist {A : Type} : Type :=
| icons : A -> ilist -> ilist.
CoFixpoint foo := (icons 3 (icons 4 foo)).
(*
So I tried doing it along the lines of how it's done for lists where it's:
[Notation "[ x ; y ; .. ; z ]" := (cons x (cons y .. (cons z nil) ..)) : list_scope.]
as mentioned at https://coq.inria.fr/refman/user-extensions/syntax-extensions.html
*)
Notation "[ x , y , .. , z , 'nil' ]" := (icons x
(icons y ..
(icons z) .. )).
(*
But this gave error:
Cannot find where the recursive pattern starts.
*)
```

How can this be fixed? Are notations possible for coinductive types in coq?

@Ju-sh the `(icons z)`

part seems off, no? It's not clear how to fix that, but I suspect you'd need to use `cofix`

so that you have a name to use in place of `nil`

(but I'm not sure of the exact syntax, https://coq.inria.fr/refman/language/core/coinductive.html#co-recursive-functions-cofix has the grammar but not an example of `cofix`

)

Thanks, a way to reference the original variable is what I needed. `cofix`

gave a way for that.

So I did

```
Notation "[ x , y , .. , z , 'NIL' ]" := (cofix Foo : ilist :=
icons x (icons y .. (icons z Foo) .. )).
(*(at level 70, no associativity). *)
Compute [ 1 , 2 , 3 , NIL ].
(* Gets error on the last closing square bracket:
Syntax error: ',' or ',' 'NIL' ']' expected (in [term]).
*)
```

Any idea where I am going off course?

okay, now we're back to the usual challenges of defining notations. To get started, it might be easier to not overload existing symbols like `[`

and `]`

— otherwise, you'll have to understand how your rule composes with the existing grammar.

Last updated: Sep 23 2023 at 08:01 UTC