More

Author: ajreynol

tests/CMakeLists.txt

@@ -144,6 +144,7 @@ set(ethos_test_file_list
     pairwise-singleton.eo
     quote-opaque.eo
     quote-requires.eo
+    set-empty-amb.eo
 )
 
 if(ENABLE_ORACLES)

tests/set-empty-amb.eo

@@ -0,0 +1,7 @@
+
+(declare-type Set (Type))
+(declare-parameterized-const set.empty ((T Type :implicit)) (Set T))
+
+(declare-type Int ())
+
+(define f () (as set.empty (Set Int)) :type (Set Int))