The Coq mailing list

[Benjamin Werner <Benjamin.Werner AT inria.fr>]

      Hello,

> 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?


If I understand you well (correct me if I am worng), you would like to
have something like (I simplify) a definition of lists where

  cons : A*list -> list

and at the same time, the product * be replaced by a record notation
(which would be specific to this version of lists).


It does seem reasonable, but I admit not having felt this need for
myself yet. I guess if the demand becomes general it should be
implemented.


Note BTW that (at least in my simple example) you do not strictly need
"Inductive with". For instance, the following definition is correct:


Inductive list [A:Set] : Set :=
   nil : (list A)
 | cons : (A*(list A))->(list A).


Best wishes,


Benjamin