helm/software/matita/tests/interactive/grafite.ma

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