mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
eacb82e5f3
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>
15 lines
525 B
Lean4
15 lines
525 B
Lean4
/- Minimized example extracted from verifying the Collatz conjecture for small numbers.
|
||
Suggested by Bhavik Mehta (@b-mehta). -/
|
||
set_option cbv.warning false
|
||
def collatzStep (n : Nat) : Nat := if n % 2 = 0 then n / 2 else (3 * n + 1) / 2
|
||
|
||
def manyStep (n m : Nat) : Nat → Bool
|
||
| 0 => false
|
||
| k + 1 => m < n ∨ manyStep n (collatzStep m) k
|
||
|
||
def checkAll (gas : Nat) : Nat → Bool
|
||
| 0 => true
|
||
| n + 1 => bif manyStep (n + 2) (n + 2) gas then checkAll gas n else false
|
||
|
||
example : checkAll 70 100 = true := by cbv
|