coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Error: "Recursive call on a non-recursive argument of constructor"

From: Andreas Abel <andreas.abel AT ifi.lmu.de>
To: Tobias Tebbi <t.tebbi AT gmail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Error: "Recursive call on a non-recursive argument of constructor"
Date: Thu, 14 Mar 2013 19:30:38 +0100

Hello Tobias,

maybe it does not lead to inconsistencies in this case (after all, it does not hurt to have one more proof of the "largest" proposition exists A:Prop. A), but it certainly is not fitting into the usual schemes of "coiteration" or "corecursion".

Best,
Andreas

On 08.03.2013 17:37, Tobias Tebbi wrote:

Hi,

The code

CoInductive foo : Prop := Box (A : Prop) : A -> foo.
CoFixpoint bar : foo := Box foo bar.

produces the error "Recursive call on a non-recursive argument of
constructor".

What is the reason for this restriction? Is there a known inconsistency
if this restriction was lifted? Or a consistency proof using this
restriction?

Thanks,

Tobias

--
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/

[Coq-Club] Error: "Recursive call on a non-recursive argument of constructor", Tobias Tebbi, 03/08/2013
- Re: [Coq-Club] Error: "Recursive call on a non-recursive argument of constructor", Andreas Abel, 03/14/2013