manual

[helm.git] / weblib / test.ma

diff --git a/weblib/test.ma b/weblib/test.ma
index 362fb6d579c872ce9de48e3ce114069851ce5c47..ab54bb5d19f1b27b8b51aee67500c82253fe8d2c 100644 (file)
--- a/weblib/test.ma
+++ b/weblib/test.ma
@@ -1,3 +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.
 
-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