coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Avoiding some unfold with simpl

From: Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>
To: Lauri Alanko <la AT iki.fi>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Avoiding some unfold with simpl
Date: Thu, 28 Oct 2010 15:06:36 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:from:date :x-google-sender-auth:message-id:subject:to:cc:content-type; b=JrcitTSR6gTW+4GradOPYtuS0Tx8TDhgH58hyE4t3CaMy3ht0ZNUV40ZjNnOpX8ylk 9F/1emm5naH4voC7K32g6Owe1MZ+Vm/dxNqTAzZguVheqMqmLKIrnuU4sdBcQWsZWTwi Q4mpc8weBzw8vOyFComgvNOUfL/PFqant1mSc=

Thanks to you and Mathieu for the trick !

To make it work in plain Coq, the notation should be

Notation "'nosimpl' t" := (let '(tt) := tt in t) (at level 10).

(let tt := tt in... does not work !)

Thanks again

Alexandre Pilkiewicz

2010/10/26 Lauri Alanko
<la AT iki.fi>:
> On Tue, Oct 26, 2010 at 01:36:53PM +0200, Alexandre Pilkiewicz wrote:
>> I would like to declare some definitions to be not unfoldable by
>> simpl, so that it doesn't go "too far".
>> I tried "Opaque myconst.", but then, even unfold fails.
>>
>> I there a better way?
>
> The ssreflect extension provides some facilities for this. See
> <http://hal.inria.fr/docs/00/40/93/56/PDF/main.pdf>, Section 7.3.
>
> Cheers,
>
>
> Lauri
>

[Coq-Club] Avoiding some unfold with simpl, Alexandre Pilkiewicz
- Re: [Coq-Club] Avoiding some unfold with simpl, Adam Chlipala
  - Re: [Coq-Club] Avoiding some unfold with simpl, Alexandre Pilkiewicz
    - Re: [Coq-Club] Avoiding some unfold with simpl, Mathieu Boespflug
- Re: [Coq-Club] Avoiding some unfold with simpl, Lauri Alanko
  - Re: [Coq-Club] Avoiding some unfold with simpl, Alexandre Pilkiewicz