helm/software/matita/tests/record.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/tests/record/".
  16
  17 record empty : Type \def {}.
  18
  19 inductive True : Prop \def I: True.
  20
  21 record pippo : Type \def
  22 {
  23 a: Set ;
  24 b: a \to Prop;
  25 c: \forall x:a.(b x) \to a \to Type
  26 }.
  27
  28 record pluto (A, B:Set) : Type \def {
  29 d: A \to B \to Prop;
  30 e: \forall y:A.\forall z:B. (d y z) \to A \to B;
  31 mario: \forall y:A.\forall z:B. \forall h:(d y z). \forall i : B \to Prop.
  32    i (e y z h y)
  33 }.
  34
  35 record paperino: Prop \def {
  36   paolo : Type;
  37   pippo : paolo \to paolo;
  38   piero : True
  39 }.
  40
  41 (* the following test used to show the following bug: the left
  42    parameter A in the type of t was not unified with the left
  43    parameter A in the type of the constructor of the record *)
  44 record t (A:Type) : Type := { f : t A }.