leanprover-community / aesop

White-box automation for Lean 4
Apache License 2.0
157 stars 25 forks source link

Set intros transparency via a ruleset, rather than an option? #73

Open semorrison opened 9 months ago

semorrison commented 9 months ago

I think the only way to change the intros transparency is via an option, which means defining a new macro if it is being used all the time.

Would it be possible to instead configure the intros transparency via rule sets?

semorrison commented 9 months ago

I guess this can be achieved by adding intro to the ruleset!

JLimperg commented 9 months ago

I'm sympathetic in principle, but not sure how to handle different definitions of the intros transparency (or other options) when multiple rule sets are active. Say the active rule sets are r1, r2. We could

But none of these approaches strikes me as generally correct.