parameter sintax added to axiom statement

[helm.git] / helm / software / components / ng_kernel / test.ma

diff --git a/helm/software/components/ng_kernel/test.ma b/helm/software/components/ng_kernel/test.ma
index 36a2d9f722cb7485d43613344acb86caa718cef2..ff017315c685abc8b3b177565e65e8fe9eb93b23 100644 (file)
--- a/helm/software/components/ng_kernel/test.ma
+++ b/helm/software/components/ng_kernel/test.ma
@@ -12,15 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-inductive nat : Set \def
-| O : nat
-| S : nat -> nat.
-
-let rec a m n :=
-match m with
- [ O => n
- | S x => S (a x n)].
+include "nat/plus.ma".
 
+(*
 let rec f n := 
   match n with
   [ O => O
@@ -30,21 +24,21 @@ let rec f n :=
              | S q => 
                   let rec h y := 
                     match y with 
-                    [ O => a (f m) (g q)
+                    [ O => f m + g q
                     | S w => h w]
                   in
                     h q] 
            in 
              g m].
+*)
 
-coinductive conat : Set \def
-| OO : conat
-| OS : conat -> conat.
-
-inductive wrap : Set \def
-| w : conat -> wrap
-| ws : wrap -> wrap.
-
-let corec h (n:nat) \def
-g (ws (w (h n)))
-and g x \def OO.
\ No newline at end of file
+let rec f n := 
+  match n with
+  [ O => O
+  | S m => g m
+  ]
+and g m :=
+ match m with
+  [ O => O
+  | S n => f n
+  ].
\ No newline at end of file