Tell Aesop to use a custom simp set #213
Description
Hello! Is there a way to tell Aesop to use a custom simp set (as defined by Lean.Meta.registerSimpAttr) instead of the default one?
The issue is that there are a few lemmas that are in the default simp context that I'd like to ignore when running a custom aesop tactic I'm writing, and I'd like a portable way to swap out the set of lemmas that simp has access to.