Aesop? ?

Stream: general

[Kevin Buzzard]

A student was working on algebraic geometry in my office today and they were at that irritating "every line takes 5 seconds to process" stage. I then noticed that they'd solved three goals earlier with aesop_cat so we changed them to sorry and all of a sudden our lives were much better. When tidy used to pull this stunt I'd change it to tidy? and then just fill in the tactic proof it found instead. Can we pull off the same trick with aesop_cat? (and then of course have aesop says ... later on :-) )

[Jannis Limperg]

aesop? already works (most of the time). If aesop_cat? doesn't work yet, we just need another macro that passes along the ?.

[Matthew Ballard]

Due to laziness, I ended up expanding aesop_cat to aesop? [rules..] but Jannis is correct that this should be fixed (easily) properly

[Matthew Ballard]

#6044 with aesop_cat?, aesop_graph?, and restrict_tac?.