The Coq mailing list

[Thorsten Altenkirch <txa AT Cs.Nott.AC.UK>]

On 11 Oct 2009, at 00:23, Vladimir Voevodsky wrote:

> Excuse me, there was a typo. The correct text is:
>
> > > Inductive I1 : Type := x0 : I1 | x1 : I1 | i : eq x0 x1 .
>
> What I want here is a type  such that for any type T, a function I1 - 
> > T is given by a triple -- t1:T (its value on x0), t2:T (its value  
> on x1) and e : eq t1 t2 .

Assuming that eq means equals, aren't two values which are the same  
not the same as one value?

T.


> Also, the definition of Impl given below is meaningless.
>
> V.
>
>
>
> On Oct 10, 2009, at 5:42 PM, Adam Chlipala wrote:
>
> > Vladimir Voevodsky wrote:
> > > Is there a way in Coq to make definitions such as:
> > >
> > > Inductive I1 : Type := x0 : I1 | x1 : I1 | i : eq x0 x1 .
> > >
> > > or
> > >
> > > Inductive Impl : Type := P1: Prop | P2: Prop | impl: P1 -> P2 .
> >
> > Neither of these fits the spirit of inductive definitions.  In each  
> > example, you might want to assert the final "constructor" as an  
> > [Axiom] instead, but there is almost always a better way to do such  
> > things.  We can't comment on the better way(s) for your specific  
> > situation without more background.
> >
> > --------------------------------------------------------
> > 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
>
> --------------------------------------------------------
> 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


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.