coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Julin S <julinshaji01 AT gmail.com>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Notation for a coinductive type
- Date: Thu, 28 Oct 2021 23:20:22 +0530
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=julinshaji01 AT gmail.com; spf=Pass smtp.mailfrom=julinshaji01 AT gmail.com; spf=None smtp.helo=postmaster AT mail-ed1-f50.google.com
- Ironport-hdrordr: A9a23:Ve7VVqBb+sJvi9vlHemT55DYdb4zR+YMi2TDGXoBMCC9E/bo7/xG+c5w6faaskd1ZJhNo6HjBEDEewK+yXcX2+gs1NWZLW3bUQKTRekI0WKh+V3d8kbFh4lgPMlbAs5D4R7LYWSST/yW3OB1KbkdKRC8npyVuQ==
- Ironport-phdr: A9a23:XBOAthAvv7RFQxO8QELDUyQUXEMY04WdBeb1wqQuh78GSKm/5ZOqZBWZua81yg6QFtiEo9t/yMPu+5j6XmIB5ZvT+FsjS7drEyE/tMMNggY7C9SEA0CoZNTjbig9AdgQHAQ9pyLzPkdaAtvxaEPPqXOu8zESBg//NQ1oLejpB4Lelcu62/6u95HJZwhEmTWxbLNwIR6rsQjfq84ajJd4JK0s0BXJuHxIe+pXxWNsO12emgv369mz8pB+7Sleouot+MFcX6r0eaQ4VqFYAy89M28p/s3rtALMQhWJ63ABT2gZiBtIAwzC7BHnQpf8tzbxu+Rh1CWGO8D9ULY5Uimg4ah2Uh/lkCgIOT43/m/Ul8J+kr5UrQm7qBBj2YPZep2ZOOZ8c67bYNgURXBBXsFUVyFZBo28co8PD+sHPe1Fsof2ulwDrRmjBQmoBePvzCRIhn/s0q040uQtDRzK0RcvH9ILqnvUrdH1OL0OXuCyyanF1DPOZO5Z1jnh8obHaAwhoe2SUrJqd8rc0VQiGh3Zg1iUqoHoOy2Z2+sQv2WG8eZuVf6ihmA6pgxyrDaj29kgh4fUiowbxF7K+yp3zJo2KNC6VUJ1bsKpHZ9WuiqHNIV2WtsvT390tCs+0LELup62cDIUxJg7xBPTcfyKf5SO7xn+TuieOy14i2hgeL+nhxa970ygyurkW8mxyllKry5FnsDSuX8QyhDf88aHR/th8ku71jaP0AfT6u5AIU8qj6bUN5khwrsompoSt0TMADP2lV3ogKOKckgo4Oul5uT9brn4upORNJV4hwHiPqg2n8ywG+U4MgwAX2iB/uS80aXu/U/kQLVOj/02lLLZsJDAKsQZp661HxJZ350s6xa6FTim0dAYkWMbI1JCfRKLl5LpNE3WIPDkEfe/hEyhnytsx/DfJ7HuHpHNLmXYn7r6ZrZ860tcyBIpwtxF5pJUDKsBIPPpVUPrutzYFExxDwvhyOH+Td55y4k2WGSVA6bfPrmBn0WP47cNPu2NYscu8GL/Nvwk4eXuhH04wQY1cqyg3J9RY3e9SKc1a36FaGbh149SWVwBuRAzGbSCYLKqXjtaZnL0VKU5tGhT4GeOAoLKR4Tri7uEjn/T9nx+Y2lHDhWBHS6tedjcHfgLby2WL4lqlTlWDdCc
Hi. I had a doubt about making notations for coinductive types in coq.
I made something like a list that keeps repeating using `CoInductive`
vernacular with
```
CoInductive ilist {A : Type} : Type :=
| icons : A -> ilist -> ilist.
```
and I can construct its objects without error:
```
(* a list like [[3;4; 3;4; 3;4; 3;4; .....]] *)
CoFixpoint foo := (icons 3 (icons 4 foo)).
```
I wanted to make a notation to easily construct the `ilist` without resorting
to chaining together constructors manually each time.
I was aiming for a notation that will allow constructing the same list as above
with: `[[ 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 in coq.
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 [constr:operconstr]).
*)
```
What am I missing here?
I made something like a list that keeps repeating using `CoInductive`
vernacular with
```
CoInductive ilist {A : Type} : Type :=
| icons : A -> ilist -> ilist.
```
and I can construct its objects without error:
```
(* a list like [[3;4; 3;4; 3;4; 3;4; .....]] *)
CoFixpoint foo := (icons 3 (icons 4 foo)).
```
I wanted to make a notation to easily construct the `ilist` without resorting
to chaining together constructors manually each time.
I was aiming for a notation that will allow constructing the same list as above
with: `[[ 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 in coq.
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 [constr:operconstr]).
*)
```
What am I missing here?
- [Coq-Club] Notation for a coinductive type, Julin S, 10/28/2021
Archive powered by MHonArc 2.6.19+.