Ssreflect Users Discussion List

[Jason Gross <>]

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