From 35be38f22657bf00344e34fe75d7f3a5283832c1 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 5 May 2005 14:15:51 +0000 Subject: [PATCH] test_instance.ma --- helm/matita/tests/test_instance.ma | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 helm/matita/tests/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 -- 2.39.2