helm/matita/tests/test4.ma

   1
   2 (* commento che va nell'ast, ma non viene contato
   3     come step perche' non e' un executable
   4 *)
   5
   6 alias num (instance 0) = "natural number".
   7 alias symbol "eq" (instance 0) = "leibnitz's equality".
   8 theorem a:0=0.
   9
  10 (* nota *)
  11 (**
  12
  13
  14 apply Prop.
  15 *)
  16 apply cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1).
  17
  18 (* commenti che non devono essere colorati perche'
  19    non c'e' nulla di eseguibile dopo di loro
  20 *)
  21 qed.