a3cb39eac9
This PR migrates most remaining tests to the new test suite. It also completes the migration of directories like `tests/lean/run`, meaning that PRs trying to add tests to those old directories will now fail.
34 lines
877 B
Text
34 lines
877 B
Text
def ackermann (n m : Nat) := match n, m with
|
|
| 0, m => m + 1
|
|
| .succ n, 0 => ackermann n 1
|
|
| .succ n, .succ m => ackermann n (ackermann (n + 1) m)
|
|
termination_by?
|
|
--^ codeAction
|
|
|
|
-- Check hat we print this even if there is only one plausible measure
|
|
def onlyOneMeasure (n : Nat) := match n with
|
|
| 0 => 0
|
|
| .succ n => onlyOneMeasure n
|
|
termination_by?
|
|
--^ codeAction
|
|
|
|
def anonymousMeasure : Nat → Nat
|
|
| 0 => 0
|
|
| .succ n => anonymousMeasure n
|
|
termination_by?
|
|
--^ codeAction
|
|
|
|
-- Check hat we print this even if there is only one plausible measure
|
|
def onlyOneMeasureWF (n : Nat) := match n with
|
|
| 0 => 0
|
|
| .succ n => onlyOneMeasureWF n
|
|
termination_by?
|
|
--^ codeAction
|
|
decreasing_by decreasing_tactic
|
|
|
|
def anonymousMeasureWF : Nat → Nat
|
|
| 0 => 0
|
|
| .succ n => anonymousMeasureWF n
|
|
termination_by?
|
|
--^ codeAction
|
|
decreasing_by decreasing_tactic
|