limiting tactics used by automated proof search tactics

Stream: lean4

[Paige Thomas]

I was just wondering, do any of the proof search tactics that output a list of tactics, like aesop, allow you to specify a restriction on the tactics that you want it to use?

[Jannis Limperg]

Aesop is fully configurable, so you can choose exactly which tactics it tries to use. (By default, it doesn't use that many tactics.)

[Paige Thomas]

Cool. Thank you.