Leonardo de Moura bba35e4532 perf: add performance comparison tests for SymM vs MetaM (#11838) ... This PR adds performance comparison tests between the new `SymM` monad and the standard `MetaM` for `intros`/`apply` operations. The tests solve problems of the form: ```lean let z := 0; ∀ x, ∃ y, x = z + y ∧ let z := z + x; ∀ x, ∃ y, x = z + y ∧ ... ∧ True ``` using repeated `intros` and `apply` with `Exists.intro`, `And.intro`, `Eq.refl`, and `True.intro`. **Results show 10-20x speedup:** | Size | MetaM | SymM | Speedup | |------|-------|------|---------| | 1000 | 226ms | 21ms | 10.8x | | 2000 | 582ms | 44ms | 13.2x | | 3000 | 1.08s | 72ms | 15.0x | | 4000 | 1.72s | 101ms | 17.0x | | 5000 | 2.49s | 125ms | 19.9x | | 6000 | 3.45s | 157ms | 22.0x |		2025-12-30 02:42:04 +00:00
..
bench	fix: update naming of FinitenessRelation fields in the sigmaIterator.lean benchmark (#11836)	2025-12-29 23:13:13 +00:00
bench-radar
compiler
elabissues
ir
lake	fix: lake: meta import transitivity (#11683)	2025-12-16 08:28:52 +00:00
lean	perf: add performance comparison tests for SymM vs MetaM (#11838)	2025-12-30 02:42:04 +00:00
pkg	chore: ensure every pkg/ test has a correct lean-toolchain file (#11782)	2025-12-23 17:17:22 +00:00
playground
plugin
simpperf
.gitignore
common.sh	feat: module system is no longer experimental (#11637)	2025-12-12 21:20:26 +00:00
lakefile.toml	feat: module system is no longer experimental (#11637)	2025-12-12 21:20:26 +00:00
lean-toolchain