From ec4cb37d34479fa36e852b9077de5025ab5297ad Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 14 Oct 2020 10:15:27 +0100 Subject: [PATCH] feat(tactic/converter): Add an exact tactic, to allow dropping back into tactic mode --- src/tactic/converter/interactive.lean | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/tactic/converter/interactive.lean b/src/tactic/converter/interactive.lean index ab8c4d54cc7f5..5b6b04f0e4b49 100644 --- a/src/tactic/converter/interactive.lean +++ b/src/tactic/converter/interactive.lean @@ -112,6 +112,19 @@ We use this tactic for writing tests. meta def guard_target (p : parse texpr) : conv unit := do `(%%t = _) ← target, tactic.interactive.guard_expr_eq t p +/-- +When using `rw` in `conv` mode on conditional equality lemmas, sometimes `⊢` goals can be +introduced which are impossible to close with `conv` tactics. Note that goals like `⊢ a = 0` will +be displayed by conv mode as `| a`, making the problem difficult to diagnose at times. + +The `exact` conv tactic allows these to be closed, and is sufficient to allow re-entering tactic +mode with `exact by { ... }`. + +Discussion of how to fix `rw` in the longer term can be found in +https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Closing.20.60.E2.8A.A2.60.20goals.20in.20.60conv.60.20mode/near/212181256 +-/ +meta def exact := tactic.interactive.exact + end interactive end conv