The Coq mailing list

[Christine Paulin <Christine.Paulin AT lri.fr>]

Dear Hiroyuki Miyoshi,

It would be interesting to have an exemple of what you want to
modelise with mutual record.
The record are supposed to be non recurive, actually a recursive
record (because it is defined inductively) will in general lead to an
empty type.

A recursive record should be defined as a coinductive type.
As mentioned by Benjamin, you may first define your records
parameterised by the recursive type 
        Record R1 [X,Y:..] := {l1:X; l2:Y}
and then use a coinductive def 
        CoInductive X : Set := c1 : (R1 X Y)->X 
        with Y : Set : ... -> Y

Christine Paulin

In his message of Mon January 22, 2001, Hiroyuki Miyoshi writes: 
> 
> Dear all,
> 
> I am using V.6.3.1 to define some higher-dimensional algebras
> and feel inconvenience of lacking for mutually-defined Records
> (definable as a macro of "Inductive ... with").
> Is that syntax planned to be provided?
> 
> Best regards,
> 
> Hiroyuki Miyoshi

-- 
  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
  INRIA tel : (+33) (0)1 39 63 54 60       fax : (+33) (0)1 39 63 56 84