coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Problems with Program.

From: Taral <taralx AT gmail.com>
To: Matthieu Sozeau <Matthieu.Sozeau AT lri.fr>
Cc: Adam Koprowski <adam.koprowski AT gmail.com>, Coq Club <coq-club AT pauillac.inria.fr>
Subject: Re: [Coq-Club] Problems with Program.
Date: Wed, 25 Mar 2009 11:49:06 -0700
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type:content-transfer-encoding; b=FVarotZ0q/FxbfimFIXHeQXo3lDHDznHVjr/QRHaa/Xhez0yCRLNykeBhqAaIAWd91 GhYMR/5kCsgFwkgPYU64G0vpXy23rER5Kw4+qfxn59aXc0bM98J59ubunbA8lRit5dFC T08LOvc5ChHQvooSZFH6Lckmuf9TqGMgO4Yls=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Wed, Mar 25, 2009 at 7:55 AM, Matthieu Sozeau
<Matthieu.Sozeau AT lri.fr>
wrote:
> P.S.: and there's a workaround too:

Neat workaround.

I tried to solve this for fun, and was forced at once point to use
proof irrelevance. Ew. Anyone know a way that doesn't use that?

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

[Coq-Club] Problems with Program., Adam Koprowski
- Re: [Coq-Club] Problems with Program., Matthieu Sozeau
  - Re: [Coq-Club] Problems with Program., Matthieu Sozeau
    - Re: [Coq-Club] Problems with Program., Taral
      - Re: [Coq-Club] Problems with Program., Adam Chlipala
- <Possible follow-ups>
- Re: [Coq-Club] Problems with Program., Santiago Zanella