helm/matita/tests/comments.ma

   1 %% commento segato dal lexer
   2
   3 (* commento che va nell'ast, ma non viene contato
   4     come step perche' non e' un executable
   5 *)
   6
   7 alias num (instance 0) = "natural number".
   8 alias symbol "eq" (instance 0) = "leibnitz's equality".
   9 theorem a:0=0.
  10
  11 %% commento segato dal lexer
  12 (* nota *)
  13
  14 %% questo lo si vuole tenere anche dopo la hint
  15 hint.
  16
  17 (* commenti che non devono essere colorati perche'
  18    non c'e' nulla di eseguibile dopo di loro
  19 *)
  20
  21 %% EOF