[Merged by Bors] - feat(topology/tactic): optionally make continuity verbose with ?

[jesse-michael-han]

---

[kim-em]

I'm not convinced this gives more useful results than the generic show_term { continuity }.

[jesse-michael-han]

Sure, this is just for convenience. continuity is a thin wrapper around tidy, so why not expose the ? available in the tidy API?

[kim-em]

But isn't it just going to print apply_rules continuity, perhaps interleaved with refine continuous.comp _ _?

[jesse-michael-han]

Yes, by definition, it will only print tactics which were available to that particular invocation of tidy. Maybe there will be more continuity tactics in the future; in any case, I think it's convenient to be able to query tidy when I know it's being called.

[kim-em]

Could you give an example where the output from continuity? is useful?

I'm hesitant to tack on ? modes for tactics unless they do something better than what show_term can do, and while I absolutely agree that's the case for tidy, I'm not seeing it yet for continuity.

[jesse-michael-han]

OK, it seems like you're saying that ? modes should be as helpful as show_term when possible.

I updated the PR so that continuity? is now equivalent to show_term {continuity}. Hopefully you will agree that being able to write ? is a convenient alternative to typing out show_term { ... }.

If, in the future, there is (say) a continuity tactic which calls simp under the hood and makes show_term not so pleasant, then we can revert to emitting the tidy trace.

[robertylewis]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Run tests