The Coq mailing list

[Jean-Christophe Filliatre <Jean-Christophe.Filliatre AT lri.fr>]

Sébastien Hinderer writes:
 > 
 > I'd like to declare two record types t1 and t2, with t1 having a field of
 > type t2, and t2 having a field of type t1.
 > Is this possible in Coq, and how ?

There is no syntax for mutually recursive records (I agree there could
be  some). But  since  "Record" is  simply  a syntactic  sugar for  an
inductive type, just replace your records by mutually inductive types:

  << Record u:Set := { A:t } with t:Set := { B:u }. >>

  -->
 
  Inductive u:Set := A:t->u with t:Set := B:u->t.

-- 
Jean-Christophe