coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] about dependent destruction in Coq 8.3

From: Gyesik Lee <gslee AT ropas.snu.ac.kr>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] about dependent destruction in Coq 8.3
Date: Tue, 14 Dec 2010 00:24:20 +0900
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:from:date:x-google-sender-auth:message-id :subject:to:content-type; b=c8RvBX3A18dE/Qk1vJXFvkByjYCD2KWyY1MUIBosjrZpz8L/Sfkteq44lZ0d6MitpJ 53+HYt/cLkHecVCs75wKf6lqVrVEPUL36T+woXHuD0Ah3XDfzydIjMZF5zj/KRaImM8x Jw6M4c71MpFHPEmJZ6BX25uoLUTadud8dLE28=

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. ?

Many thanks in advance.

Gyesik

[Coq-Club] about dependent destruction in Coq 8.3, Gyesik Lee
- Re: [Coq-Club] about dependent destruction in Coq 8.3, Matthieu Sozeau