coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Tobias Tebbi <t.tebbi AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Error: "Recursive call on a non-recursive argument of constructor"
Date: Fri, 8 Mar 2013 17:37:20 +0100

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

[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