X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Ftest.ma;h=ab54bb5d19f1b27b8b51aee67500c82253fe8d2c;hb=db7ecce6c398a42f14557067bf18b61cf75da80e;hp=c8b89a5daf2273d6fdc13c42d740c194bb73522f;hpb=e593e93ca00c6e9dfb8f0e79cb52684c5b104c3f;p=helm.git

diff --git a/weblib/test.ma b/weblib/test.ma
index c8b89a5da..ab54bb5d1 100644
--- a/weblib/test.ma
+++ b/weblib/test.ma
@@ -1,5 +1,8 @@
-(* prova *)
+inductive nat : Set ≝
+| O : nat
+| S : nat span class="error" title="Parse error: SYMBOL '.' expected after [grafite_ncommand] (in [executable])"span class="error" title="Parse error: SYMBOL '.' expected after [grafite_ncommand] (in [executable])"span class="error" title="Parse error: SYMBOL '.' expected after [grafite_ncommand] (in [executable])"→/span/span/span nat.
 
-(* prova 2 *)
-
-axiom pippo : Prop.
\ No newline at end of file
+let rec plus n m ≝
+match n with
+[O ⇒ m
+|(S p) ⇒ S (plus p m)].
\ No newline at end of file