From 7d1c9a278b160a9f6ab5fc6fec98d5e8e78e465e Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 10 Jun 2005 16:57:50 +0000
Subject: [PATCH] added_test

---
 helm/matita/tests/record.ma | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)
 create mode 100644 helm/matita/tests/record.ma

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
-- 
2.39.2