From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 5 May 2005 14:15:51 +0000 (+0000)
Subject: test_instance.ma
X-Git-Tag: single_binding~107
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=35be38f22657bf00344e34fe75d7f3a5283832c1;p=helm.git

test_instance.ma
---

diff --git a/helm/matita/tests/test_instance.ma b/helm/matita/tests/test_instance.ma
new file mode 100644
index 000000000..cb3aa3fb2
--- /dev/null
+++ b/helm/matita/tests/test_instance.ma
@@ -0,0 +1,4 @@
+instance \lambda A:Set.\lambda P:A \to A \to Prop.\forall x:A. P x x.
+instance \lambda A:Set.\lambda P:A \to A \to Prop.\forall x,y:A. P x y \to P y x.
+instance \lambda A:Set.\lambda P:A \to A \to Prop.\forall x,y,z:A. P x y \to P y z \to P y z.
+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