coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Apply argument to fix-expression

From: Andreas Lundblad <landreas AT kth.se>
To: Coq Mailing List <coq-club AT pauillac.inria.fr>
Subject: Re: [Coq-Club] Apply argument to fix-expression
Date: Sat, 19 Sep 2009 14:57:00 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:date :x-google-sender-auth:message-id:subject:from:to:content-type; b=S3hzIe6ffE/JeRJSLCwBEC/oFVy9qh4Z6lEDpGtIs1qrAP6qNmNXRtVtTsL3VWIoBu wHkBOqX24jevgkgfvFWQf+1/Ckqig6iONruFcyJRkw1PaSfFhLEyVXCAmZry3Qr9/n9R rQAdyLTFRfk8KZS4qi9MxRCdlKAGvR0IuvdWU=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Rewriting it as a [fun] worked fine. Thanks.

My original problem was actually not on lists, but on a data type with
a large number of constructors. I didn't want to use [destruct] since
it generated a lot of cases, which I thought was completely
unnecessary since the required fact ([nth 2 l 7] in the above case)
was independent of the constructor.

Best regards,
Andreas Lundblad

[Coq-Club] Apply argument to fix-expression, Andreas Lundblad
- Re: [Coq-Club] Apply argument to fix-expression, Adam Chlipala
  - Re: [Coq-Club] Apply argument to fix-expression, Andreas Lundblad
    - Re: [Coq-Club] Apply argument to fix-expression, Stéphane Glondu