lean4-htt/tests
Leonardo de Moura 2f3939f1ea
fix: incorrect grind param warning (#11194)
This PR the redundant `grind` parameter warning message. It now checks
the `grind` theorem instantiation constraints too.
2025-11-15 20:17:55 +00:00
..
bench feat: verify all and any for hash maps (#10765) 2025-11-15 16:59:37 +00:00
compiler fix: use general allocator for closures (#10982) 2025-10-27 10:16:59 +00:00
elabissues
ir
lake fix: lake: indeterminism in targets test (#11188) 2025-11-15 04:20:24 +00:00
lean fix: incorrect grind param warning (#11194) 2025-11-15 20:17:55 +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
simpperf
.gitignore
common.sh chore: make workspaceSymbol benchmarks modules (#11094) 2025-11-05 18:40:39 +00:00
lakefile.toml
lean-toolchain