lean4-htt/tests
Leonardo de Moura f84aa23d6d
feat: metavar cleanup in Sym.simp (#12096)
This PR cleanups temporary metavariables generated when applying
rewriting rules in `Sym.simp`.
2026-01-21 21:36:17 +00:00
..
bench feat: metavar cleanup in Sym.simp (#12096) 2026-01-21 21:36:17 +00:00
bench-radar chore: add size/install benchmark (#12015) 2026-01-15 14:43:47 +00:00
compiler
elabissues
ir
lake chore: lake: disable import all check (for now) (#12045) 2026-01-19 22:42:22 +00:00
lean fix: symbol name for native boxed declarations in the interpreter (#12095) 2026-01-21 20:38:29 +00:00
pkg fix: split ngen on async elab (#12000) 2026-01-14 12:35:25 +00:00
playground
plugin
simpperf
.gitignore
common.sh feat: re-integrate lean4checker as leanchecker (#11887) 2026-01-08 09:41:33 +00:00
lakefile.toml
lean-toolchain