]> matita.cs.unibo.it Git - helm.git/blob - helm/matita/tests/test4.ma
added Variant theorem flavour
[helm.git] / helm / matita / tests / test4.ma
1 set "baseuri" "cic:/matita/tests/test4/".
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.