added examples

diff --git a/helm/matita/tests/test4.ma b/helm/matita/tests/test4.ma
new file mode 100644 (file)
index 0000000..4d7b03c
--- /dev/null
+++ b/helm/matita/tests/test4.ma
@@ -0,0 +1,4 @@
+alias num (instance 0) = "natural number".
+alias symbol "eq" (instance 0) = "leibnitz's equality".
+theorem a:0=0.
+reflexivity.
\ No newline at end of file

diff --git a/helm/matita/tests/test5.ma b/helm/matita/tests/test5.ma
new file mode 100644 (file)
index 0000000..928402a
--- /dev/null
+++ b/helm/matita/tests/test5.ma
@@ -0,0 +1,5 @@
+instance 
+  \lambda A:Set. 
+  \lambda f: A \to A \to A.
+  \forall x,y : A.
+      f x y = f y x.
\ No newline at end of file

diff --git a/helm/matita/tests/test6.ma b/helm/matita/tests/test6.ma
new file mode 100644 (file)
index 0000000..c6a935a
--- /dev/null
+++ b/helm/matita/tests/test6.ma
@@ -0,0 +1,5 @@
+instance 
+  \lambda A:Set.
+  \lambda f:A \to A \to A.
+  \forall x,y,z:A.
+   f x (f y z) = f (f x y) z.
\ No newline at end of file

diff --git a/helm/matita/tests/test7.ma b/helm/matita/tests/test7.ma
new file mode 100644 (file)
index 0000000..3fc609d
--- /dev/null
+++ b/helm/matita/tests/test7.ma
@@ -0,0 +1,5 @@
+instance 
+  \lambda A:Set.
+  \lambda r:A \to A \to Prop.
+  \forall x:A.
+   r x x.
\ No newline at end of file