Def Mathlib.Tactic.optConfigOf

Modification history

2026-05-29 13:23
Mathlib/Tactic/ApplyWith.lean
chore: bump toolchain to v4.31.0-rc1 (#39980)
Deleted Mathlib.Tactic.optConfigOfView on Github →
2026-02-06 14:32
Mathlib/Tactic/ApplyWith.lean
fix(Tactic/ApplyWith): disambiguate parse to improve error messages (#34721) …
Added Mathlib.Tactic.optConfigOfView on Github →