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

[eric-wieser]

---

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Closing.20.60.E2.8A.A2.60.20goals.20in.20.60conv.60.20mode/near/212181256

I no longer have any PRs which depend on this.

This would be a stop-gap until leanprover-community/lean#475 is resolved.

[fpvandoorn]

What happens when you apply this to a conv-goal? Ideally there would be an understandable error message.

[eric-wieser]

Well, exact rfl behaves exactly the same as skip in conv mode.

[urkud]

Could you please add a test case?

[fpvandoorn]

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

[eric-wieser]

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.

[fpvandoorn]

Ah, ok, so usually a goal | t means t = ?m? That would also be useful to note in the docstring of the exact tactic. Something like "The goal | t means t = ?m, which means that you can use the tactic exact h whenever h has type t = s."

[robertylewis]

I second the requests for tests and additional doc comments. This looks fine to me as a stopgap. Longer term I think we should reexamine the conv implementation and documentation. I find it inconvenient and annoying so I mostly try to avoid it myself.

[YaelDillies]

This is now a different problem in Lean 4 (does it need solving?). To be revisited after the port.