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 set "baseuri" "cic:/matita/tests/comments/".
  16
  17 (* commento che va nell'ast, ma non viene contato
  18     come step perche' non e' un executable
  19 *)
  20
  21 alias num (instance 0) = "natural number".
  22 alias symbol "eq" (instance 0) = "leibnitz's equality".
  23 theorem a:0=0.
  24
  25 (* nota *)
  26 (**
  27
  28
  29 apply Prop.
  30 *)
  31 reflexivity.
  32 (* commenti che non devono essere colorati perche'
  33    non c'e' nulla di eseguibile dopo di loro
  34 *)
  35 qed.