coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Well-formed condition for fixpoints in Coq 6.3

From: Marino Miculan <miculan AT dimi.uniud.it>
To: coq-club AT pauillac.inria.fr
Subject: Well-formed condition for fixpoints in Coq 6.3
Date: Wed, 8 Sep 1999 17:23:15 +0200 (CEST)

Hi all,

as it is described in the changelog, Coq V6.3 allows for inductive
definitions with nested recursion, as

  Inductive term : Set :=  c : (list term)->term

But the CC(Co)Ind described in Chapter 4 of the Reference Manual does not
allow for these definitions - so I suppose that the manual is outdated.

Where can I find a formal description of the new CC(Co)Ind, and in
particular, of the new treatment of fixpoint definitions?

Thanks in advance,
- Marino

--
   Marino Miculan    - Dipartimento di Matematica e Informatica
Universita' di Udine - via delle Scienze 206 - 33100 Udine - Italy
tel. +39-043255-8456 - fax +39-043255-8499 (attn. Miculan)
mailto:miculan AT dimi.uniud.it
     http://www.dimi.uniud.it/~miculan

Well-formed condition for fixpoints in Coq 6.3, Marino Miculan