coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Re: Applying a definition

From: "N. Raghavendra" <raghu AT hri.res.in>
To: coq-club AT inria.fr
Subject: [Coq-Club] Re: Applying a definition
Date: Mon, 12 Aug 2013 03:25:30 +0530
Cancel-lock: sha1:S3L/dTeTPOp6DG5nWZTRVZcua28=

At 2013-08-11T11:19:27-04:00, Adam Chlipala wrote:

> A shorter proof script is
> destruct b; auto.

Thank you. I should read about `auto'. (It isn't in the first chapter
of Software Foundations, where the exercise occurs.)

Best regards,
Raghu.

--
N. Raghavendra
<raghu AT hri.res.in>,
http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/

[Coq-Club] Applying a definition, N. Raghavendra, 08/10/2013
- Re: [Coq-Club] Applying a definition, Andrew Hirsch, 08/10/2013
  - [Coq-Club] Re: Applying a definition, N. Raghavendra, 08/10/2013
    - Re: [Coq-Club] Re: Applying a definition, Adam Chlipala, 08/11/2013
      - [Coq-Club] Re: Applying a definition, N. Raghavendra, 08/11/2013