helm/matita/tests/test4.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
  15
  16 %% questo lo si vuole tenere anche dopo la hint
  17 hint.
  18 **)
  19 apply cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1).
  20
  21 (* commenti che non devono essere colorati perche'
  22    non c'e' nulla di eseguibile dopo di loro
  23 *)
  24 qed.
  25 %% EOF