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

diff --git a/weblib/test.ma b/weblib/test.ma
index 362fb6d57..ab54bb5d1 100644
--- a/weblib/test.ma
+++ b/weblib/test.ma
@@ -1,3 +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.
 
-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