coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Matthieu Sozeau <mattam AT mattam.org>
- To: Gyesik Lee <gslee AT ropas.snu.ac.kr>
- Cc: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] about dependent destruction in Coq 8.3
- Date: Tue, 14 Dec 2010 19:24:49 +0100
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=sender:subject:mime-version:content-type:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to:x-mailer; b=PGEgDAguua+jhOLT9dUlOjzqqkcJbNby3gXvlEtOrGbvLQp8v7sEaGKSXMZo6KcKb7 VhQlMYvknSvHHj4G9fvsCWn45IDlxmtp1c3F7dCzZbGJUnHaB763o8FbYxurgwxnv/1F BDueWYgeX1JdWGKcIYWesPc3xxVzfEuesx7Tw=
Le 13 déc. 2010 à 16:24, Gyesik Lee a écrit :
> Hi,
>
> it seems that the behavior of applying "dependent destruction" has
> changed a lot with Coq 8.3. compared to 8.2.
> Are there any examples showing a good application of dependent
> destruction, dependent induction etc. ?
Hi Gyesik,
there's a few examples in test-suite/success/dependentind.v. Sadly,
the currently released 8.3 version suffers from a few bugs that were
resolved since.
Hope this helps,
-- Matthieu
- [Coq-Club] about dependent destruction in Coq 8.3, Gyesik Lee
- Re: [Coq-Club] about dependent destruction in Coq 8.3, Matthieu Sozeau
Archive powered by MhonArc 2.6.16.