Ssreflect Users Discussion List

[Georges Gonthier <>]

  You would have to write down the alternative explicitly (rewrite {1}/foo /foo /bar || rewrite {1}/bar /bar); obviously, this won’t scale too well if you have too many such definitions. You might want to use unfold, which will interoperate better with progress, for this sort of Ltac hacking (the Ssreflect rewrite .. in .. is designed to work with general rewrite rules on possibly dependent assumptions – it would have been a little difficult to preserve low-level primitives such as progress in such generality).

 

From: Jason Gross [mailto:]
Sent: 07 July 2014 11:44
To: Georges Gonthier
Cc: ssreflect
Subject: Re: [ssreflect] Correct way to do "progress rewrite /foo in H"?

 

What if I want to do [progress rewrite /foo/bar in H]?  That is, I want there to be at least one occurrence of either foo or bar.

 

On Mon, Jul 7, 2014 at 11:41 AM, Georges Gonthier <> wrote:

Perhaps rewrite {1}/foo /foo in H ? (the {1} checks that there is at least one occurrence to unfold).

 - Georges

 

From: [mailto:] On Behalf Of Jason Gross
Sent: 07 July 2014 11:24
To: ssreflect
Subject: [ssreflect] Correct way to do "progress rewrite /foo in H"?

 

Hi,

Is there a "correct" way to do [progress rewrite /foo in H]?  That invocation doesn't work, because [rewrite /foo in H] will move H to the bottom even if it does nothing else.  I can do [move H at bottom; progress rewrite /foo in H], but that seems a bit hackish.

 

Thanks,

Jason