diff options
| author | Vincent Laporte | 2019-08-05 08:28:49 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-08-05 08:34:33 +0000 |
| commit | 08c9ac8e0919ed7e6c001542c2094640f1d7bd73 (patch) | |
| tree | cf063f71553697ca8f7f0bef888eb18bcad62834 | |
| parent | c9efc722c559ca315dda890cf2d5cc8e934b8ad2 (diff) | |
ConstructiveCauchyReals: make explicit structural recursion
| -rw-r--r-- | theories/Reals/ConstructiveCauchyReals.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Reals/ConstructiveCauchyReals.v b/theories/Reals/ConstructiveCauchyReals.v index 5a0f4abec7..3ca9248600 100644 --- a/theories/Reals/ConstructiveCauchyReals.v +++ b/theories/Reals/ConstructiveCauchyReals.v @@ -1144,7 +1144,7 @@ Proof. - intro abs. apply (CReal_plus_lt_compat_l r) in abs. contradiction. Qed. -Fixpoint BoundFromZero (qn : nat -> Q) (k : nat) (A : positive) +Fixpoint BoundFromZero (qn : nat -> Q) (k : nat) (A : positive) {struct k} : (forall n:nat, le k n -> Qlt (Qabs (qn n)) (Z.pos A # 1)) -> { B : positive | forall n:nat, Qlt (Qabs (qn n)) (Z.pos B # 1) }. Proof. |