added_test

diff --git a/helm/matita/tests/record.ma b/helm/matita/tests/record.ma
new file mode 100644 (file)
index 0000000..43e8e5d
--- /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