diff --git a/test/Typecheck/Positive.hs b/test/Typecheck/Positive.hs index 462cc64530..625955e4ff 100644 --- 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 new file mode 100644 index 0000000000..7e2e10f382 --- /dev/null +++ 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@{};