Zulip Chat Archive
Stream: lean4
Topic: Is there a `scoped attribute [-simp]` foo?
Eric Wieser (Aug 19 2025 at 11:59):
I have a scope that adds some simp lemmas which conflict with existing simp lemmas. Can that same scope disable the existing ones?
Yaël Dillies (Aug 19 2025 at 12:00):
That would be very useful for #26057 too
Last updated: Dec 20 2025 at 21:32 UTC