From 7c08187b8e1af81817927151aa07d52b72c7aa4d Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 3 May 2005 13:40:53 +0000
Subject: [PATCH] added examples

---
 helm/matita/tests/test4.ma | 4 ++++
 helm/matita/tests/test5.ma | 5 +++++
 helm/matita/tests/test6.ma | 5 +++++
 helm/matita/tests/test7.ma | 5 +++++
 4 files changed, 19 insertions(+)
 create mode 100644 helm/matita/tests/test4.ma
 create mode 100644 helm/matita/tests/test5.ma
 create mode 100644 helm/matita/tests/test6.ma
 create mode 100644 helm/matita/tests/test7.ma

diff --git a/helm/matita/tests/test4.ma b/helm/matita/tests/test4.ma
new file mode 100644
index 000000000..4d7b03ce2
--- /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
index 000000000..928402a53
--- /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
index 000000000..c6a935a88
--- /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
index 000000000..3fc609da4
--- /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
-- 
2.39.2