helm/matita/tests/record.ma

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