Skip to content

GitLab

I
Iris
Closed
Opened by Dan Frumin@dfruminContributor
Report abuse New issue

Document `iRewrite -...` in `ProofMode.md`

I would like to be able to say something like iRewrite <- "Heq" so that it would transform the goal

"Heq": R ≡ Q
-------------*
Q

into

-------------*
R
Edited by Robbert