add/remove (default := true) for aesop rule sets

Stream: metaprogramming / tactics

[Chris Henson]

If I declare an aesop rule set with (default := true), can I later add/remove this?

[Jannis Limperg]

This is not supported at the moment. Addition could be supported fairly easily. Removal would work only locally, similar to local attribute [-simp] foo. This is how attribute removal generally works in Lean because otherwise the default rule sets might start to depend on import order. Would this work for you?

[Chris Henson]

Yes, that would be perfect.

[Jannis Limperg]

aesop#243