X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Ftest.ma;h=ab54bb5d19f1b27b8b51aee67500c82253fe8d2c;hb=7d699d63675466675b854fac8364de5a4887e6b2;hp=c8b89a5daf2273d6fdc13c42d740c194bb73522f;hpb=b0bce111aa8d2b50d07151fe54e45e564874d727;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