matita/components/ng_kernel/test.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "nat/plus.ma".
  16
  17 (*
  18 let rec f n :=
  19   match n with
  20   [ O => O
  21   | S m => let rec g x :=
  22              match x with
  23              [ O => f m
  24              | S q =>
  25                   let rec h y :=
  26                     match y with
  27                     [ O => f m + g q
  28                     | S w => h w]
  29                   in
  30                     h q]
  31            in
  32              g m].
  33 *)
  34
  35 let rec f n :=
  36   match n with
  37   [ O => O
  38   | S m => g m
  39   ]
  40 and g m :=
  41  match m with
  42   [ O => O
  43   | S n => f n
  44   ].