Commit 2026-02-06 14:32 b4b6732f

View on Github →

fix(Tactic/ApplyWith): disambiguate parse to improve error messages (#34721) This PR fixes that apply and applyWith have overlapping parses, which seems to cause bad error messages ("this declaration contains sorry" instead of "apply failed, type mismatch"). Zulip threads:

https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/Wall.20of.20warnings.20of.20.60unreachableTactic.60.2F.60unusedTactic.60
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/optConfig.20causes.20tactics.20to.20be.20ignored/with/571416569

Estimated changes

Modified Mathlib/Tactic/ApplyWith.lean

added def Mathlib.Tactic.getManyConfigItems

added def Mathlib.Tactic.optConfigOf

Modified MathlibTest/apply_with.lean

added theorem MyProp.mk

added def MyProp