coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] another question (cont.)

From: Taral <taralx AT gmail.com>
To: Vladimir Voevodsky <vladimir AT ias.edu>
Cc: Coq Club <coq-club AT pauillac.inria.fr>
Subject: Re: [Coq-Club] another question (cont.)
Date: Tue, 13 Oct 2009 13:48:03 -0700
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type:content-transfer-encoding; b=Th4xvt9Yq9oUtePWrqqZE653va954o6TgDeX9aYwBy7wwlPJyHjYvPgcYDSh+xfNHw 9PPqWEkqYaabnA8+13kvZuuCo2fl911mHQkzMRCOmB3kIbAcWHX7CaMVxKq4beSPyZyb Zbt8x/w+V+gjzUnBsNLKhzO53va4s8MFtDgMU=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Tue, Oct 13, 2009 at 10:57 AM, Vladimir Voevodsky
<vladimir AT ias.edu>
wrote:
> Actually,
>
> Check eq S0 P0 .
>
> produces
>
> S0 = P0
> � � : Prop
>
> Is this a bug?

Nope. Just implicits biting you.

Coq < Check @eq Set P0 S0.
P0 = S0
: Prop

--
Taral
<taralx AT gmail.com>
"Please let me know if there's any further trouble I can give you."
-- Unknown

Re: [Coq-Club] an inductive types question, (continued)