From 068cc700d8540728558556bf6f86ff6988478d91 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 11 Jan 2022 15:03:07 -0800 Subject: [PATCH] test: ackermann --- tests/lean/run/ack.lean | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 tests/lean/run/ack.lean diff --git a/tests/lean/run/ack.lean b/tests/lean/run/ack.lean new file mode 100644 index 0000000000..6ec3751f40 --- /dev/null +++ b/tests/lean/run/ack.lean @@ -0,0 +1,5 @@ +def ack : Nat → Nat → Nat + | 0, y => y+1 + | x+1, 0 => ack x 1 + | x+1, y+1 => ack x (ack (x+1) y) +termination_by' PSigma.lex sizeOfWFRel (fun _ => sizeOfWFRel)