lean4-htt/tests
Cameron Zwarich 8d0093b43f
fix: properly handle scoping of join point candidates in cce (#7398)
This PR fixes a scoping error in the cce (Common Case Elimination) pass
of the old code generator. This pass would create a join point for
common minor premises even if some of those premises were in the bodies
of locally defined functions, which results in an improperly scoped
reference to a join point. The fix is to save/restore candidates when
visiting a lambda.
2025-03-08 18:10:41 +00:00
..
bench perf: optimize sorry detection in unused variables linter (#7129) 2025-02-22 16:43:39 +00:00
compiler feat: cleanup of get and back functions on List/Array (#7059) 2025-02-17 01:43:45 +00:00
elabissues
ir
lean fix: properly handle scoping of join point candidates in cce (#7398) 2025-03-08 18:10:41 +00:00
pkg feat: debug_assert! (#7256) 2025-03-03 16:34:44 +00:00
playground chore: remove save tactic (#7047) 2025-02-12 09:19:30 +00:00
plugin
simpperf
.gitignore
common.sh
lean-toolchain