add test

anoma · Jan 29, 2025 · 5801acb · 5801acb
1 parent ecc5689
commit 5801acb
Show file tree

Hide file tree

Showing 2 changed files with 30 additions and 0 deletions.
diff --git a/test/Typecheck/Positive.hs b/test/Typecheck/Positive.hs
@@ -184,6 +184,10 @@ tests =
       "Basic lambda functions"
       $(mkRelDir "Internal")
       $(mkRelFile "Lambda.juvix"),
+    posTest
+      "AnomaSet"
+      $(mkRelDir "Internal")
+      $(mkRelFile "AnomaSet.juvix"),
     posTest
       "Simple mutual inference"
       $(mkRelDir "Internal")

diff --git a/tests/positive/Internal/AnomaSet.juvix b/tests/positive/Internal/AnomaSet.juvix
@@ -0,0 +1,26 @@
+module AnomaSet;
+
+type Bool :=
+  | false
+  | true;
+
+builtin list
+type List a :=
+  | nil
+  | cons a (List a);
+
+Logic : Type := Instance -> Bool;
+
+builtin anoma-set
+axiom AnomaSet : Type -> Type;
+
+builtin anoma-set-to-list
+axiom anomaSetToList {A} (set : AnomaSet A) : List A;
+
+type Resource :=
+  mkResource@{
+    logic : Logic;
+  };
+
+positive
+type Instance := mkInstance@{};