helm/software/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 inductive nat : Set \def
  16 | O : nat
  17 | S : nat -> nat.
  18
  19 let rec a m n :=
  20 match m with
  21  [ O => n
  22  | S x => S (a x n)].
  23
  24 let rec f n :=
  25   match n with
  26   [ O => O
  27   | S m => let rec g x :=
  28              match x with
  29              [ O => f m
  30              | S q =>
  31                   let rec h y :=
  32                     match y with
  33                     [ O => a (f m) (g q)
  34                     | S w => h w]
  35                   in
  36                     h q]
  37            in
  38              g m].
  39
  40 coinductive conat : Set \def
  41 | OO : conat
  42 | OS : conat -> conat.
  43
  44 inductive wrap : Set \def
  45 | w : conat -> wrap
  46 | ws : wrap -> wrap.
  47
  48 let corec h (n:nat) \def
  49 g (ws (w (h n)))
  50 and g x \def OO.