helm/matita/tests/interactive/grafite.ma

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