Julin S (Oct 02 2021 at 12:15): Julin S (Oct 02 2021 at 12:15):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?
Paolo Giarrusso (Oct 02 2021 at 12:21):@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
Paolo Giarrusso (Oct 02 2021 at 12:22):(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)
Julin S (Oct 02 2021 at 13:10):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?
Paolo Giarrusso (Oct 02 2021 at 13:23):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