Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

feat(tactic/converter): Add an exact tactic, to allow dropping back into tactic mode #4615

Closed
eric-wieser wants to merge 1 commit into from
Closed

feat(tactic/converter): Add an exact tactic, to allow dropping back into tactic mode #4615

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 13 additions & 0 deletions src/tactic/converter/interactive.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Comment on lines +117 to +118
Copy link
Member

@fpvandoorn fpvandoorn Oct 15, 2020

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this fixable, by checking whether the RHS is a metavariable when displaying the goal?

Copy link
Member Author

@eric-wieser eric-wieser Oct 15, 2020 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think the fix would have to be within lean itself. That would certainly be better than what happens today, but it doesn't strike me as exhaustive.


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

Expand Down