coq-club AT inria.fr

Subject: The Coq mailing list

List archive

mutually-defined Records

From: Hiroyuki Miyoshi <hxm AT cc.kyoto-su.ac.jp>
To: coq-club AT pauillac.inria.fr
Cc: hxm AT cc.kyoto-su.ac.jp
Subject: mutually-defined Records
Date: Mon, 22 Jan 2001 03:45:37 +0900

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

mutually-defined Records, Hiroyuki Miyoshi
- Re: mutually-defined Records, Benjamin Werner
- Re: mutually-defined Records, Christine Paulin
  - Re: mutually-defined Records, Hiroyuki Miyoshi