coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] positivity check

From: Andreas Abel <andreas.abel AT ifi.lmu.de>
To: David Monniaux <David.Monniaux AT imag.fr>, coq-club AT inria.fr
Subject: Re: [Coq-Club] positivity check
Date: Wed, 02 Oct 2013 16:01:24 -0400

On 27.09.2013 04:03, David Monniaux wrote:

CoInductive foo (X : Type) :=
| Moo : X -> (foo (foo X)) -> foo X.

But then I get:

Error: Non strictly positive occurrence of "foo" in
"X -> foo (foo X) -> foo X".

Isn't this check a bit too strict? My remembrances on the positivity
check in (co)inductive datatypes is hazy, but I don't see how this
construction could create inconsistencies.

Yes, it is too strict.

Agda allows your type; it has a more sophisticated positivity checker.

Cheers,
Andreas

--
Andreas Abel <>< Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel AT ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/

Re: [Coq-Club] positivity check, Andreas Abel, 10/02/2013