(* *)
(**************************************************************************)
-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
| 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