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.

Estimated changes