lean4-htt/tests
Cameron Zwarich c292ae2e0e
fix: don't create reduced arity LCNF decls with no params (#7086)
This PR makes the arity reduction pass in the new code generator match
the old one when it comes to the behavior of decls with no used
parameters. This is important, because otherwise we might create a
top-level decl with no params that contains unreachable code, which
would get evaluated unconditionally during initialization. This actually
happens when initializing Init.Core built with the new code generator.
2025-02-27 01:23:34 +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: don't create reduced arity LCNF decls with no params (#7086) 2025-02-27 01:23:34 +00:00
pkg feat: smarter plugin loading (#7090) 2025-02-18 23:03:52 +00:00
playground chore: remove save tactic (#7047) 2025-02-12 09:19:30 +00:00
plugin
simpperf
.gitignore
common.sh
lean-toolchain