what does this ltac definition do?
Ltac rewr_assumption := idtac; match goal with
| [R: _ = _ |- _ ] => first [rewrite R| rewrite <- R]
Can you explain it in plain English?
It checks the context for an equality R and tries to rewrite using it. If rewriting along the equality doesn't work it then tries rewriting back then gives up.
rewrite R there is an implicit
rewrite -> R (from left to right). So it tries to use
R both ways.
I'm however not sure why idtac is there. Presumably it does nothing here.
Also, before giving up, it will look for another equality to rewrite with.
This is probably the "thunk idiom", I'm not an exprert but
idtac; tac do, in some context, behave like ML code
tac () and
fun () -> tac () (in ML these two expressions don't have the same type, but in Ltac1 they do, fixed in Ltac2). I suspect the
idtac is there to be sure the
match-goal-with is evaluated when you expect it.
Re "gives up", that tactic will give up by failing, if there's no equality in context where rewriting succeeds, no?
Last updated: Jan 27 2023 at 01:03 UTC