Ssreflect Users Discussion List

[Georges Gonthier <>]

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