coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Mutually dependent records

From: Christine Paulin <Christine.Paulin AT lri.fr>
To: Jean-Christophe.Filliatre AT lri.fr (Jean-Christophe Filliatre)
Cc: S�bastien Hinderer <Sebastien.Hinderer AT ens-lyon.fr>, Coq <coq-club AT pauillac.inria.fr>
Subject: Re: [Coq-Club] Mutually dependent records
Date: Wed, 9 Jul 2003 14:35:15 +0200
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

The point is that a record structure is usually supposed to be non
recursive. A recursive record is often empty
(except if the recursive argument of the constructor has a functional
type), and should rather be defined co-inductively.
I strongly recommand to avoid the record structure in that case and
use the alternative (Co)Inductive syntax
C. Paulin

--
  Christine Paulin-Mohring             mailto :
Christine.Paulin AT lri.fr
  LRI, UMR 8623 CNRS, Bat 490, Universit� Paris Sud,   91405 ORSAY Cedex
  LRI   tel : (+33) (0)1 69 15 66 35       fax : (+33) (0)1 69 15 65 86

[Coq-Club] Mutually dependent records, S�bastien Hinderer
- Re: [Coq-Club] Mutually dependent records, Jean-Christophe Filliatre
  - Re: [Coq-Club] Mutually dependent records, Christine Paulin