lean4-htt/tests
Henrik Böving e9ccdeecd0
perf: add a benchmark for simp on local hypotheses (#9403)
This PR adds a benchmark to our suite, specifically targeting the fact
that local hypotheses
are currently not indexed in simp and can thus cause significant
slowdowns compared to having them
as external declarations.
2025-07-16 12:16:29 +00:00
..
bench perf: add a benchmark for simp on local hypotheses (#9403) 2025-07-16 12:16:29 +00:00
compiler
elabissues
ir
lean perf: use IR type info to decide whether to insert RC ops (#9396) 2025-07-16 02:02:32 +00:00
pkg feat: prettier expected type mismatch error message (#9099) 2025-07-01 07:50:53 +00:00
playground refactor: migrate all usages of old slice notation (#9000) 2025-06-27 18:52:07 +00:00
plugin
simpperf
.gitignore
common.sh
lakefile.toml
lean-toolchain