Stream: math-comp users

Topic: revert/move


view this post on Zulip Laurent Théry (May 19 2021 at 13:50):

Is there an ssreflect equivalent of revert (move: x doesn't make it) here :

Goal let x := 1 in x * x = 1.
move=> x; revert x.

view this post on Zulip Pierre-Yves Strub (May 19 2021 at 13:52):

move: @x ?

view this post on Zulip Pierre-Yves Strub (May 19 2021 at 13:53):

I remember having seen a syntax for that (I assume you want to keep the def. of x here)

view this post on Zulip Laurent Théry (May 19 2021 at 13:53):

thanks! didn't know it exists


Last updated: Oct 13 2024 at 01:02 UTC