lean4-htt/tests
Cameron Zwarich 820c1e6f15
chore: remove tests that recompile builtin definitions (#9523)
In the early days of the new compiler, it was common to make tests that
manually compiled a definition with the new compiler. The arity
reduction pass in LCNF deliberately does not compute a fixed point to
find a minimal set of used parameters for performance reasons, but
running it a second time can lead to different decisions being made and
a decl arity mismatch. This has been an issue for multiple people during
development. Removing the tests fixes the problem.

Fixes #9186.
2025-07-25 04:37:33 +00:00
..
bench perf: phashmap benchmark (#9517) 2025-07-24 14:57:07 +00:00
compiler
elabissues
ir
lean chore: remove tests that recompile builtin definitions (#9523) 2025-07-25 04:37:33 +00:00
pkg perf: do not export specializations (#9465) 2025-07-23 13:12:15 +00:00
playground
plugin
simpperf
.gitignore
common.sh
lakefile.toml
lean-toolchain