helm/matita/tests/record.ma

   1 record empty : Type \def {}.
   2
   3 record pippo : Type \def
   4 {
   5 a: Set ;
   6 b: a \to Prop;
   7 c: \forall x:a.(b x) \to a \to Type
   8 }.
   9
  10 record pluto (A, B:Set) : Type \def {
  11 d: A \to B \to Prop;
  12 e: \forall y:A.\forall z:B. (d y z) \to A \to B;
  13 mario: \forall y:A.\forall z:B. \forall h:(d y z). \forall i : B \to Prop.
  14    i (e y z h y)
  15 }.
  16
  17 record paperino: Prop \def {
  18   paolo : Type;
  19   pippo : paolo \to paolo;
  20   piero : True
  21 }.