From 2f10ba8dbe8e73226e913c508a94fba84a50594e Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Wed, 13 Nov 2024 15:26:06 +0100
Subject: [PATCH] add tests

---
 test/Termination/Positive.hs             | 10 +++++++++-
 tests/positive/Termination/Nested1.juvix | 11 +++++++++++
 tests/positive/Termination/Nested2.juvix | 16 ++++++++++++++++
 3 files changed, 36 insertions(+), 1 deletion(-)
 create mode 100644 tests/positive/Termination/Nested1.juvix
 create mode 100644 tests/positive/Termination/Nested2.juvix

diff --git a/test/Termination/Positive.hs b/test/Termination/Positive.hs
index f1fc4ca5ce..b8194d0055 100644
--- a/test/Termination/Positive.hs
+++ b/test/Termination/Positive.hs
@@ -67,7 +67,15 @@ tests =
     PosTest
       "Ignore instance arguments"
       $(mkRelDir ".")
-      $(mkRelFile "issue2414.juvix")
+      $(mkRelFile "issue2414.juvix"),
+    PosTest
+      "Nested local definitions"
+      $(mkRelDir ".")
+      $(mkRelFile "Nested1.juvix"),
+    PosTest
+      "Named arguments"
+      $(mkRelDir ".")
+      $(mkRelFile "Nested2.juvix")
   ]
 
 testsWithKeyword :: [PosTest]
diff --git a/tests/positive/Termination/Nested1.juvix b/tests/positive/Termination/Nested1.juvix
new file mode 100644
index 0000000000..4c3bab7b18
--- /dev/null
+++ b/tests/positive/Termination/Nested1.juvix
@@ -0,0 +1,11 @@
+module Nested1;
+
+import Stdlib.Data.List open;
+
+go {A B} (f : A -> B) : List A -> List B
+  | nil := nil
+  | (elem :: next) :=
+    let
+      var1 := f elem;
+      var2 := go f next;
+    in var1 :: var2;
diff --git a/tests/positive/Termination/Nested2.juvix b/tests/positive/Termination/Nested2.juvix
new file mode 100644
index 0000000000..bfbe1f3fd8
--- /dev/null
+++ b/tests/positive/Termination/Nested2.juvix
@@ -0,0 +1,16 @@
+module Nested2;
+
+type MyList A :=
+  | myNil
+  | myCons@{
+      elem : A;
+      next : MyList A;
+    };
+
+go {A B} (f : A -> B) : MyList A -> MyList B
+  | myNil := myNil
+  | myCons@{elem; next} :=
+    myCons@{
+      elem := f elem;
+      next := go f next;
+    };