lean4-htt/tests
Cameron Zwarich 2e627d3692 feat: move constructor layout to Lean and add a few optimizations
This PR moves the constructor layout code from C++ to Lean. When
writing the new compiler, we just reused the existing C++ code,
even though it was a bit inconvenient, because we wanted to
ensure that constructor layout always matched the existing
compiler.

This fixes #2589 by handling struct field types just like any
other type being lowered, and thus applying the trivial structure
optimization in the process. Originally, I wanted to port the
code to Lean without any functional changes, but I found that
it took less code to just implement it "correctly" and get this
fix as a consequence than to emulate the bugs of the existing
C++ implementation.
2025-06-30 15:39:58 +02:00
..
bench refactor: migrate all usages of old slice notation (#9000) 2025-06-27 18:52:07 +00:00
compiler fix: avoid caching uses of never_extract constants in toLCNF (#8956) 2025-06-24 02:04:56 +00:00
elabissues
ir
lean feat: move constructor layout to Lean and add a few optimizations 2025-06-30 15:39:58 +02:00
pkg feat: make private the default in module (#9044) 2025-06-28 16:30: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