coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] unfold _ in _ ?

From: Beta Ziliani <beta AT mpi-sws.org>
To: Coq Club <coq-club AT inria.fr>
Cc: Vladimir Voevodsky <vladimir AT ias.edu>
Subject: Re: [Coq-Club] unfold _ in _ ?
Date: Wed, 25 Feb 2015 18:08:19 -0300

If you use Ssreflect, Ssreflect's rewrite allows you to do this (and more).

On Wed, Feb 25, 2015 at 5:56 PM, Vladimir Voevodsky <vladimir AT ias.edu> wrote:

Hello,

is there a way to say “unfold ident" in "subexp.” as one can say “change subexp with exp.” ?

Of course, one can not use the word “in” here but there does not seem to be any other reason not to have such a feature.

Vladimir.

[Coq-Club] unfold _ in _ ?, Vladimir Voevodsky, 02/25/2015
- Re: [Coq-Club] unfold _ in _ ?, Beta Ziliani, 02/25/2015
- Re: [Coq-Club] unfold _ in _ ?, Jonathan Leivent, 02/25/2015