weblib/test.ma

   1 inductive nat : Set ≝
   2 | O : nat
   3 | 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.
   4
   5 let rec plus n m ≝
   6 match n with
   7 [O ⇒ m
   8 |(S p) ⇒ S (plus p m)].