diff options
Diffstat (limited to 'theories/PArith/BinPosDef.v')
-rw-r--r-- | theories/PArith/BinPosDef.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v index 4541fce0d..aed4fef05 100644 --- a/theories/PArith/BinPosDef.v +++ b/theories/PArith/BinPosDef.v @@ -195,16 +195,16 @@ Infix "*" := mul : positive_scope. (** ** Iteration over a positive number *) -Fixpoint iter (n:positive) {A} (f:A -> A) (x:A) : A := - match n with +Definition iter {A} (f:A -> A) : A -> positive -> A := + fix iter_fix x n := match n with | xH => f x - | xO n' => iter n' f (iter n' f x) - | xI n' => f (iter n' f (iter n' f x)) + | xO n' => iter_fix (iter_fix x n') n' + | xI n' => f (iter_fix (iter_fix x n') n') end. (** ** Power *) -Definition pow (x y:positive) := iter y (mul x) 1. +Definition pow (x:positive) := iter (mul x) 1. Infix "^" := pow : positive_scope. @@ -488,13 +488,13 @@ Definition shiftr_nat (p:positive) := nat_rect _ p (fun _ => div2). Definition shiftl (p:positive)(n:N) := match n with | N0 => p - | Npos n => iter n xO p + | Npos n => iter xO p n end. Definition shiftr (p:positive)(n:N) := match n with | N0 => p - | Npos n => iter n div2 p + | Npos n => iter div2 p n end. (** Checking whether a particular bit is set or not *) |