helm/matita/tests/test4.ma

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