From 7d699d63675466675b854fac8364de5a4887e6b2 Mon Sep 17 00:00:00 2001 From: matitaweb Date: Tue, 10 Apr 2012 17:15:08 +0000 Subject: [PATCH] commit by user --- weblib/test.ma | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) 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 -- 2.39.2