clean up examples vs tests

6 files changed, 37 insertions, 0 deletions

diff --git a/examples/tests/test_alpha_equiv.makkai b/examples/tests/test_alpha_equiv.makkai
new file mode 100644
index 0000000..2ae067a
--- /dev/null
+++ b/examples/tests/test_alpha_equiv.makkai
@@ -0,0 +1,4 @@
+let signature S = (n : Nat) -> Set
+let signature T = (m : Nat) -> Set
+let instance i :: S = for (x : Nat), (Nat :: Set)
+let instance j :: T = i
diff --git a/examples/tests/test_ext_codomain.makkai b/examples/tests/test_ext_codomain.makkai
new file mode 100644
index 0000000..da0ddae
--- /dev/null
+++ b/examples/tests/test_ext_codomain.makkai
@@ -0,0 +1,5 @@
+let signature S = (x : Nat) -> theory { G :: Set }
+
+let instance s :: S = for (x : Nat), { .G = (Nat :: Set) }
+
+let set NatAgain = set-of((s 42) .G)
diff --git a/examples/tests/test_inline_nested.makkai b/examples/tests/test_inline_nested.makkai
new file mode 100644
index 0000000..e891349
--- /dev/null
+++ b/examples/tests/test_inline_nested.makkai
@@ -0,0 +1,9 @@
+let signature Outer = theory {
+    Inner :: theory { F :: Set }
+}
+
+let instance my_outer :: Outer = {
+    .Inner = { .F = (Nat :: Set) }
+}
+
+let set MyF = set-of(my_outer .Inner .F)
diff --git a/examples/tests/test_nested_for.makkai b/examples/tests/test_nested_for.makkai
new file mode 100644
index 0000000..b3618cc
--- /dev/null
+++ b/examples/tests/test_nested_for.makkai
@@ -0,0 +1,3 @@
+let signature F = (n : Nat) -> (m : Nat) -> Set
+let instance f :: F = for (n : Nat), for (m : Nat), (Nat :: Set)
+let set Result = set-of(f 1 2)
diff --git a/examples/tests/test_signature_merge.makkai b/examples/tests/test_signature_merge.makkai
new file mode 100644
index 0000000..5f575d5
--- /dev/null
+++ b/examples/tests/test_signature_merge.makkai
@@ -0,0 +1,12 @@
+let signature S = (n : Nat) -> Set
+let signature U = (k : Bool) -> S
+let signature W = (k : Bool)(n : Nat) -> Set
+
+let instance u :: U = for (k : Bool), for (n : Nat), (Nat :: Set)
+let instance w :: W = u
+
+let signature F = (n : Nat) (m : Nat) -> Set
+let signature G = (n : Nat) -> (m : Nat) -> Set
+
+let instance f :: F = for (n : Nat) (m : Nat), (Nat :: Set)
+let instance g :: G = f
diff --git a/examples/tests/test_signature_param.makkai b/examples/tests/test_signature_param.makkai
new file mode 100644
index 0000000..9dae31b
--- /dev/null
+++ b/examples/tests/test_signature_param.makkai
@@ -0,0 +1,4 @@
+let signature S = theory {
+  F :: (x : Nat) (y : Bool) -> Set,
+  G :: (z : set-of(F 3 4)) -> Set // this sould fail
+}