lean4-htt

40408 commits 1 branch 0 tags 5.3 GiB

Author SHA1 Message Date

Author	SHA1	Message	Date
Wojciech Różowski	5cc6585c9b	chore: disable `cbv` usage warning (#12986 ) This disables `cbv` usage warning and reflects that in the corresponding unit tests.	2026-03-19 14:12:04 +00:00
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

Wojciech Różowski

5cc6585c9b

chore: disable cbv usage warning (#12986 )

This disables `cbv` usage warning and reflects that in the corresponding
unit tests.

2026-03-19 14:12:04 +00:00

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

Renamed from tests/lean/run/cbv4.lean (Browse further)

2 commits