helm/matita/tests/comments.ma

   1 (****************************************************************************)
   2 (*       ___                                                                *)
   3 (*      ||M||                                                               *)
   4 (*      ||A||       A project by Andrea Asperti                             *)
   5 (*      ||T||                                                               *)
   6 (*      ||I||       Developers:                                             *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                            *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                   *)
   9 (*      \   /                                                               *)
  10 (*       \ /        This file is distributed under the terms of the         *)
  11 (*        v         GNU General Public License Version 2                    *)
  12 (*                                                                          *)
  13 (****************************************************************************)
  14
  15 (* commento che va nell'ast, ma non viene contato
  16     come step perche' non e' un executable
  17 *)
  18
  19 alias num (instance 0) = "natural number".
  20 alias symbol "eq" (instance 0) = "leibnitz's equality".
  21 theorem a:0=0.
  22
  23 (* nota *)
  24 (**
  25
  26
  27 apply Prop.
  28 *)
  29 reflexivity.
  30 (* commenti che non devono essere colorati perche'
  31    non c'e' nulla di eseguibile dopo di loro
  32 *)
  33 qed.