Skip to content

GitLab

Closed
Opened by Dan Frumin@dfruminContributor

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 Krebbers