Commit 2025-04-30 14:55 c8dd6259
View on Github →chore: use modern config syntax (#24469)
For example, simp +contextual
is much more readable than simp (config := { contextual := true })
.
This PR replaces about 150 occurrences; mathlib has another 200 occurrences remaining. (Two dozen of those are from the "apply with" tactic, which doesn't support modern syntax yet.)
Helps with auto-formatting: the spacing was not quite uniform in mathlib.