Commit 2026-03-16 00:46 fde0cc50

View on Github →

feat(Tactic/FastInstance): use expected type to fill in arguments (#36420) This PR improves fast_instance% by letting it use the expected type to fill in arguments. This allows us to then define inferInstanceAs% A as a macro for fast_instance% inferInstanceAs A.

Estimated changes

Modified Mathlib/Algebra/Order/Ring/StandardPart.lean

Modified Mathlib/NumberTheory/Padics/WithVal.lean

Modified Mathlib/Order/BooleanAlgebra/Set.lean

Modified Mathlib/Tactic/FastInstance.lean

deleted def Mathlib.Elab.FastInstance.elabFastInstance

added def Mathlib.Elab.FastInstance.error

Modified MathlibTest/DefEqAbuse.lean

Created MathlibTest/InferInstanceAsPercent.lean

added def MyNat

added def TestNat

added def myNatInv_leaky

added def testField_direct

added def testField_fixed

added def testField_leaky

Modified MathlibTest/fast_instance.lean

Modified MathlibTest/slow_instances.lean