helm/matita/tests/record.ma

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