lean4-htt/tests/lean
Wojciech Różowski eacb82e5f3
test: move cbv tests to appropriate directories (#12791)
This PR moves cbv tests to the correct test directories. `cbv4.lean` is
a
straightforward elaboration test and is moved to `tests/elab/`. The AES
and ARM
load/store tests are performance-oriented stress tests and are moved to
`tests/elab_bench/`.

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
2026-03-04 15:53:05 +00:00
..
docparse fix: error messages from Verso docstring parser (#12372) 2026-02-07 07:49:06 +00:00
grind chore: prefer cons_cons over cons₂ in names (#12710) 2026-02-27 08:58:08 +00:00
interactive perf: add high priority to OfSemiring.Q instances (#12782) 2026-03-04 12:58:15 +00:00
run test: move cbv tests to appropriate directories (#12791) 2026-03-04 15:53:05 +00:00
server
sym feat: add Goal API for SymM + grind (#12143) 2026-01-24 20:30:08 +00:00
copy-produced
test_single.sh