helm/matita/tests/interactive/grafite.ma

   1 %% test per matita.lang
   2
   3 set "baseuri" "cic:/matita/tests/".
   4
   5 %% commento
   6 (* commento *)
   7 (** hint. **)
   8
   9 inductive pippo : Type \def
  10   | a : Type \to pippo
  11   | b : Prop \to pippo
  12   | c : Set \to pippo.
  13
  14 definition pollo : Set \to Set \def
  15   \lambda a:Set.a.
  16
  17 inductive paolo : Prop \def t:paolo.
  18
  19 theorem comeno : \forall p:pippo.pippo.
  20 intros.assumption.
  21 qed.
  22
  23 definition f : pippo \to paolo \def
  24   \lambda x:pippo.
  25   match x with
  26   [ (a z) \Rightarrow t
  27   | (b z) \Rightarrow t
  28   | (c z) \Rightarrow t ].
  29
  30 record w : Type \def {
  31   mario : Prop;
  32   pippo : Set
  33 }.
  34
  35 whelp locate pippo.
  36
  37 print "coercions".
  38
  39
  40