add tests

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]

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;

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;
+    };