From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 10 Jun 2005 16:57:50 +0000 (+0000)
Subject: added_test
X-Git-Tag: PRE_STORAGE~66
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7d1c9a278b160a9f6ab5fc6fec98d5e8e78e465e;p=helm.git

added_test
---

diff --git a/helm/matita/tests/record.ma b/helm/matita/tests/record.ma
new file mode 100644
index 000000000..43e8e5d44
--- /dev/null
+++ b/helm/matita/tests/record.ma
@@ -0,0 +1,21 @@
+record empty : Type \def {}.
+
+record pippo : Type \def 
+{
+a: Set ;
+b: a \to Prop;
+c: \forall x:a.(b x) \to a \to Type 
+}.
+
+record pluto (A, B:Set) : Type \def {
+d: A \to B \to Prop;
+e: \forall y:A.\forall z:B. (d y z) \to A \to B;
+mario: \forall y:A.\forall z:B. \forall h:(d y z). \forall i : B \to Prop.
+   i (e y z h y)
+}.
+
+record paperino: Prop \def {
+  paolo : Type;
+  pippo : paolo \to paolo;
+  piero : True
+}.
\ No newline at end of file