coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Coq User <coquser AT googlemail.com>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] Recursive call on a non-recursive argument of constructor
Date: Mon, 24 Aug 2009 21:05:51 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=googlemail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type; b=VH/X6gSBqMTrnXnJaFAA4Pu9Gm+geu6Z+07cOiJcASzcUJDWFJH3I4MngddRDUSa7e BCvFFgjwOVWSvxQPoBANpjzz3w8eodXhgkXrHhlWbUBT4h0PRa4oJnU63+jp+8wLrE4s WdWcUiqy7csnw7rZDlpmcxHumyu4rV48nq0So=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Does anyone know under what conditions the error: "Recursive call on a non-recursive argument of constructor" is raised?� I'm defining some coinductive types using CoFixpoint, and this error is always raised, although the constructor arguments are the correct types.

[Coq-Club] Recursive call on a non-recursive argument of constructor, Coq User