coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Tom Harke <harke AT cs.pdx.edu>
- To: Coq User <coquser AT googlemail.com>
- Cc: coq-club AT pauillac.inria.fr, Tom Harke <harke AT cs.pdx.edu>
- Subject: Re: [Coq-Club] Re: Recursive call on a non-recursive argument of constructor
- Date: Tue, 25 Aug 2009 11:04:19 -0700
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
When you use CoFixpoint the result type must be CoInductive.
So, I can get your example to check if I change
> CoFixpoint singleton:SpecialObject :=
to
> CoFixpoint singleton:Object :=
though I don't know if this is what you want.
- [Coq-Club] Re: Recursive call on a non-recursive argument of constructor, Coq User
- Re: [Coq-Club] Re: Recursive call on a non-recursive argument of constructor, Tom Harke
Archive powered by MhonArc 2.6.16.