Leonardo de Moura 531dbf0e1b perf: mkFunExtFor (#11932) ... This PR eliminates super-linear kernel type checking overhead when simplifying lambda expressions. I improved the proof term produced by `mkFunext`. This function is used in `Sym.simp` when simplifying lambda expressions. ### Lambda benchmark: before vs after optimization | Lambda | Before simp (ms) | After simp (ms) | Simp speedup | Before kernel (ms) | After kernel (ms) | Kernel speedup | Before proof | After proof | Proof reduction | |--------|------------------|-----------------|--------------|--------------------|-------------------|----------------|--------------|-------------|-----------------| | 10 | 0.269 | 0.208 | 1.29× | 0.521 | 0.390 | 1.34× | 583 | 498 | 1.17× | | 20 | 0.457 | 0.382 | 1.20× | 1.126 | 0.651 | 1.73× | 1323 | 918 | 1.44× | | 30 | 0.747 | 0.536 | 1.39× | 1.733 | 0.789 | 2.20× | 2263 | 1338 | 1.69× | | 40 | 0.819 | 0.697 | 1.18× | 2.696 | 1.065 | 2.53× | 3403 | 1758 | 1.94× | | 50 | 1.035 | 0.901 | 1.15× | 3.918 | 1.304 | 3.01× | 4743 | 2178 | 2.18× | | 100 | 2.351 | 1.823 | 1.29× | 20.073 | 2.927 | 6.86× | 14443 | 4278 | 3.38× | | 150 | 3.920 | 2.873 | 1.36× | 60.266 | 5.290 | 11.39× | 29143 | 6378 | 4.57× | | 200 | 5.869 | 3.819 | 1.54× | 148.681 | 6.903 | 21.54× | 48843 | 8478 | 5.76× | We can now handle much larger lambda expressions. For example: lambda_1000: 20.869250ms, kernel: 98.637875ms, proof_size=42078 This new approach will be implemented in `Meta.simp` in the future. Here is the table with the `Meta.simp` numbers. ### Old `Meta.simp` lambda benchmark | Lambda | Simp time (ms) | Kernel time (ms) | Proof size | |--------|----------------|------------------|------------| | 10 | 2.308 | 0.667 | 1273 | | 20 | 5.739 | 1.817 | 3323 | | 30 | 10.687 | 3.320 | 6173 | | 40 | 17.607 | 6.326 | 9823 | | 50 | 28.336 | 9.024 | 14273 | | 100 | 137.878 | 34.344 | 48523 | | 150 | 395.429 | 77.329 | 102773 | | 200 | 866.097 | 143.020 | 177023 |		2026-01-08 04:28:58 +00:00
..
ArgsPacker
Constructions	refactor: DiscrTree (#11875)	2026-01-02 19:53:45 +00:00
DiscrTree	feat: add insertPattern for discrimination tree insertion in Sym (#11884)	2026-01-03 19:27:43 +00:00
Match	refactor: DiscrTree (#11875)	2026-01-02 19:53:45 +00:00
Sym	perf: mkFunExtFor (#11932)	2026-01-08 04:28:58 +00:00
Tactic	feat: filter out deprecated lemmas from suggestions in exact?/rw? (#11918)	2026-01-07 23:45:04 +00:00
AbstractMVars.lean
AbstractNestedProofs.lean
ACLt.lean	refactor: DiscrTree (#11875)	2026-01-02 19:53:45 +00:00
AppBuilder.lean	refactor: DiscrTree (#11875)	2026-01-02 19:53:45 +00:00
ArgsPacker.lean
Basic.lean	feat: add Meta.Context.cacheInferType (#11869)	2026-01-02 03:21:43 +00:00
BinderNameHint.lean
Canonicalizer.lean
CasesInfo.lean	chore: fix spelling (#11531)	2025-12-06 13:54:27 +00:00
Check.lean	fix: deep recursion type checking grind proof (#11061)	2025-11-02 19:43:48 +00:00
CheckTactic.lean
Closure.lean
Coe.lean	refactor: DiscrTree (#11875)	2026-01-02 19:53:45 +00:00
CoeAttr.lean
CollectFVars.lean
CollectMVars.lean
CompletionName.lean
CongrTheorems.lean	refactor: DiscrTree (#11875)	2026-01-02 19:53:45 +00:00
Constructions.lean	feat: sparse sparse casesOn splitting in match equations (#11666)	2025-12-14 14:59:45 +00:00
CtorIdxHInj.lean	feat: grind support for .ctorIdx (#11652)	2025-12-13 13:32:19 +00:00
CtorRecognizer.lean
DecLevel.lean
Diagnostics.lean
DiscrTree.lean	refactor: DiscrTree (#11875)	2026-01-02 19:53:45 +00:00
Eqns.lean	chore: fix spelling (#11531)	2025-12-06 13:54:27 +00:00
Eval.lean
ExprDefEq.lean	chore: remove leftover (#11895)	2026-01-04 21:42:13 +00:00
ExprLens.lean
ExprTraverse.lean
ForEachExpr.lean
FunInfo.lean
GeneralizeTelescope.lean
GeneralizeVars.lean
GetUnfoldableConst.lean	feat: add TransparencyMode.none (#11810)	2025-12-27 03:10:17 +00:00
GlobalInstances.lean
HasNotBit.lean	perf: use Nat-based bitmask in sparse cases construction (#11200)	2025-11-17 10:05:18 +00:00
HaveTelescope.lean	feat: add option for simplifying have decls in two passes (#11923)	2026-01-07 01:58:36 +00:00
Hint.lean	chore: rename Substring to Substring.Raw (#11154)	2025-11-16 09:30:04 +00:00
IndPredBelow.lean	chore: fix spelling (#11531)	2025-12-06 13:54:27 +00:00
Inductive.lean
InferType.lean	feat: add Meta.Context.cacheInferType (#11869)	2026-01-02 03:21:43 +00:00
Injective.lean	feat: make noConfusion even more heterogeneous	2025-12-10 17:28:06 +01:00
Instances.lean	feat: add insertPattern for discrimination tree insertion in Sym (#11884)	2026-01-03 19:27:43 +00:00
IntInstTesters.lean	fix: nonstandard instances in grind and simp +arith (#11758)	2025-12-21 17:56:49 +00:00
Iterator.lean
KAbstract.lean
KExprMap.lean
LazyDiscrTree.lean	fix: allow exact? to suggest local private declarations (part 2) (#11759)	2025-12-21 20:03:10 +00:00
LetToHave.lean
LevelDefEq.lean
LitValues.lean
Match.lean
MatchUtil.lean	refactor: make MatchEqs a leaf module (#11493)	2025-12-03 09:15:36 +00:00
MethodSpecs.lean	refactor: DiscrTree (#11875)	2026-01-02 19:53:45 +00:00
MkIffOfInductiveProp.lean
MonadSimp.lean	refactor: have telescope support (#11914)	2026-01-06 19:20:25 +00:00
NatInstTesters.lean	fix: nonstandard instances in grind and simp +arith (#11758)	2025-12-21 17:56:49 +00:00
NatTable.lean
Offset.lean	fix: nonstandard instances in grind and simp +arith (#11758)	2025-12-21 17:56:49 +00:00
Order.lean
PPGoal.lean	chore: do not set unused Option.Decl.group (#11307)	2025-11-21 16:44:38 +00:00
PProdN.lean
ProdN.lean	feat: new do elaborator, part 1: doElem_elab attribute (#11150)	2025-11-12 14:25:28 +00:00
RecursorInfo.lean
Reduce.lean
ReduceEval.lean
SameCtorUtils.lean
SizeOf.lean	refactor: DiscrTree (#11875)	2026-01-02 19:53:45 +00:00
Sorry.lean
SplitSparseCasesOn.lean	feat: sparse sparse casesOn splitting in match equations (#11666)	2025-12-14 14:59:45 +00:00
Structure.lean	refactor: DiscrTree (#11875)	2026-01-02 19:53:45 +00:00
Sym.lean	refactor: reorganize SymM and GrindM monad hierarchy (#11909)	2026-01-06 01:12:07 +00:00
SynthInstance.lean	feat: remove the group field of an option description (#11305)	2025-11-24 11:40:58 +00:00
Tactic.lean
Transform.lean	chore: fix spelling (#11531)	2025-12-06 13:54:27 +00:00
TransparencyMode.lean	feat: add TransparencyMode.none (#11810)	2025-12-27 03:10:17 +00:00
TryThis.lean	chore: rename String.ValidPos to String.Pos (#11240)	2025-11-24 16:40:21 +00:00
UnificationHint.lean	feat: add insertPattern for discrimination tree insertion in Sym (#11884)	2026-01-03 19:27:43 +00:00
WHNF.lean	perf: do not consult isNoConfusion in whnf (#11571)	2025-12-09 23:36:46 +00:00