lean4-htt/tests/lean/run
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
..
10067.lean fix: copied 11940 fix for structure command (#12680) 2026-02-25 13:50:04 +00:00
10850.lean fix: let Meta.zetaReduce zeta reduce have expressions (#12695) 2026-02-27 00:37:52 +00:00
async_http_encode.lean feat: add core HTTP data types (#12126) 2026-03-04 14:32:29 +00:00
async_http_string_quoting.lean feat: add core HTTP data types (#12126) 2026-03-04 14:32:29 +00:00
mvcgenRflReducibility.lean fix: heartbeat limit in mvcgen due to withDefault rfl (#12696) 2026-02-26 16:40:42 +00:00
ppFVarsAnonymous.lean fix: use _fvar._ instead of _ for anonymous fvars (#12745) 2026-03-01 09:59:13 +00:00
test_single.sh