trace.tauto and/or alternatives?

Stream: new members

[Craig McLaughlin]

I was wondering what the option trace.tauto is supposed to do? I thought if I set it to true and placed the point over an invocation of tauto it would provide some kind of output as to what the tactic did. However, nothing seems to happen. I am using lean4-mode with Emacs 27.1. My main desire was to find out if my theorems relied on any classical reasoning, and whilst I have since found out I can use #print axioms my_thm for that purpose, I'd like to know if I can trace the innards of tauto regardless.

[Ruben Van de Velde]

Wasn't there some command to print a proof in some kind of table form that worked well with tauto proofs?