lean4-htt/tests
Leonardo de Moura 4c189bc8f2
fix: grind actions (#11203)
This PR fixes a few minor issues in the new `Action` framework used in
`grind`. The goal is to eventually delete the old `SearchM`
infrastructure. The main `solve` function used by `grind` is now based
on the `Action` framework. The PR also deletes dead code in `SearchM`.
2025-11-17 00:37:19 +00:00
..
bench test: benchmark for large partial match (#11199) 2025-11-16 11:20:31 +00:00
compiler
elabissues
ir
lake fix: lake: indeterminism in targets test (#11188) 2025-11-15 04:20:24 +00:00
lean fix: grind actions (#11203) 2025-11-17 00:37:19 +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