Modularization of Nnat

 For instance, nat_of_Nplus is now N2Nat.inj_add

 Note that we add an iter function in BinNat.N

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14105 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 12 insertions, 4 deletions

diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v
index 535f88c86..ec91dc5db 100644
--- a/theories/NArith/BinNatDef.v
+++ b/theories/NArith/BinNatDef.v
@@ -351,14 +351,22 @@ Definition testbit a n :=
 
 Definition to_nat (a:N) :=
   match a with
-  | 0 => O
-  | Npos p => Pos.to_nat p
+    | 0 => O
+    | Npos p => Pos.to_nat p
   end.
 
 Definition of_nat (n:nat) :=
   match n with
-  | O => 0
-  | S n' => Npos (Pos.of_succ_nat n')
+    | O => 0
+    | S n' => Npos (Pos.of_succ_nat n')
+  end.
+
+(** Iteration of a function *)
+
+Definition iter (n:N) {A} (f:A->A) (x:A) : A :=
+  match n with
+    | 0 => x
+    | Npos p => Pos.iter p f x
   end.
 
 End N.
\ No newline at end of file