lean4-htt/tests/lean
Wojciech Różowski 7390024170
test: add cbv test for Collatz conjecture verification (#12692)
This PR adds a `cbv` tactic test based on a minimized example extracted
from verifying the Collatz conjecture for small numbers, suggested by
Bhavik Mehta (@b-mehta).

---------

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
2026-02-25 17:05:51 +00:00
..
docparse fix: error messages from Verso docstring parser (#12372) 2026-02-07 07:49:06 +00:00
grind
interactive chore: relative lean-toolchains (#12652) 2026-02-25 10:23:35 +00:00
run test: add cbv test for Collatz conjecture verification (#12692) 2026-02-25 17:05:51 +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