lean4-htt/tests
Joachim Breitner 09001ecad6
fix: let realizeConst run withDeclNameForAuxNaming (#11221)
This PR lets `realizeConst` use `withDeclNameForAuxNaming` so that
auxilary definitions created there get non-clashing names.
2025-11-17 21:17:16 +00:00
..
bench test: benchmark for large partial match (#11199) 2025-11-16 11:20:31 +00:00
compiler fix: consider over-applications in reduceArity compiler pass (#11185) 2025-11-17 07:51:37 +00:00
elabissues
ir
lake fix: lake: indeterminism in targets test (#11188) 2025-11-15 04:20:24 +00:00
lean fix: let realizeConst run withDeclNameForAuxNaming (#11221) 2025-11-17 21:17:16 +00:00
pkg chore: make compilation type mismatch error message from non-exposed defs a lot less mysterious (#11177) 2025-11-14 10:50:43 +00:00
playground
plugin chore: re-enable tests (#10923) 2025-10-23 08:38:57 +00:00
simpperf
.gitignore
common.sh chore: make workspaceSymbol benchmarks modules (#11094) 2025-11-05 18:40:39 +00:00
lakefile.toml
lean-toolchain