commit by user

[helm.git] / weblib / test.ma

diff --git a/weblib/test.ma b/weblib/test.ma
index c8b89a5daf2273d6fdc13c42d740c194bb73522f..ab54bb5d19f1b27b8b51aee67500c82253fe8d2c 100644 (file)
--- a/weblib/test.ma
+++ b/weblib/test.ma
@@ -1,5 +1,8 @@
-(* prova *)
+inductive nat : Set ≝
+| O : nat
+| S : nat \ 5span class="error" title="Parse error: SYMBOL '.' expected after [grafite_ncommand] (in [executable])"\ 6\ 5span class="error" title="Parse error: SYMBOL '.' expected after [grafite_ncommand] (in [executable])"\ 6\ 5span class="error" title="Parse error: SYMBOL '.' expected after [grafite_ncommand] (in [executable])"\ 6→\ 5/span\ 6\ 5/span\ 6\ 5/span\ 6 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