The Coq mailing list

[AUGER Cédric <Cedric.Auger AT lri.fr>]

As said by Adam, I am wondering if don't have confusion between Records  
and Inductives:

Le Sat, 10 Oct 2009 23:32:28 +0200, Vladimir Voevodsky <vladimir AT ias.edu>  
a écrit:

> Is there a way in Coq to make definitions such as:

what you expect in
> Inductive I1 : Type := x0 : I1 | x1 : I1 | i : eq x0 x1 .
may be:

Record I1 T := makeI1
{ x0 : T;
  x1 : T;
  i : x0 = x1
}

which is strictly the same as

Inductive I1 T :=
makeI1 : forall x0 x1, x0 = x1 -> I1 T.

Definition x0 T (x : I1 T) :=
match x with
makeI1 x0 _ _ => x0
end.

Definition x1 T (x : I1 T) :=
match x with
makeI1 _ x1 _ => x1
end.

Definition i T (x : I1 T) :=
 let (x0, x1, i) as x2 return (x0 x2 = x1 x2) := x in i.

and the .() notations
(Check it with the Print command)


> or
>
> Inductive Impl : Type := P1: Prop | P2: Prop | impl: P1 -> P2 .
>
> ?
>
> V.
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club


--
Utilisant le client e-mail révolutionnaire d'Opera :  
http://www.opera.com/mail/