Leonardo de Moura ff87bcb8e5 feat: add option for simplifying have decls in two passes (#11923) ... This PR adds a new option to the function `simpHaveTelescope` in which the `have` telescope is simplified in two passes: * In the first pass, only the values and the body are simplified. * In the second pass, unused declarations are eliminated. This new mode eliminates **superlinear** behavior in the benchmark `simp_3.lean`. Note that the kernel type checker still **exhibits** quadratic behavior in this example, because it **does not have support** for expanding a `have`/`let` telescope in a single step.		2026-01-07 01:58:36 +00:00
..
meta_simp_1.lean	chore: include free variables (#11894)	2026-01-04 18:51:18 +00:00
meta_simp_2.lean	feat: simplify lambdas in Sym.simp (#11898)	2026-01-05 01:00:30 +00:00
simp_1.lean	refactor: reorganize SymM and GrindM monad hierarchy (#11909)	2026-01-06 01:12:07 +00:00
simp_2.lean	refactor: reorganize SymM and GrindM monad hierarchy (#11909)	2026-01-06 01:12:07 +00:00
simp_3.lean	feat: add option for simplifying have decls in two passes (#11923)	2026-01-07 01:58:36 +00:00