From b9025b5b986e3243042bde2566490d37209d2c8c Mon Sep 17 00:00:00 2001
From: mohring
Date: Fri, 12 Mar 2004 10:15:44 +0000
Subject: ajout decimal_exp pour interpreter les notations decimales

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5464 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Reals/Rfunctions.v | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index 188699e6d1..4fcde3833f 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -658,6 +658,14 @@ intros n1 H'; rewrite Rinv_mult_distr; try rewrite Rinv_1; try rewrite H';
  auto with real.
 Qed.
 
+(*******************************)
+(* For easy interface          *)
+(*******************************)
+(* decimal_exp r z is defined as r 10^z *)
+ 
+Definition decimal_exp (r:R) (z:Z) : R := (r * 10 ^Z z).
+
+
 (*******************************)
 (** Sum of n first naturals    *)
 (*******************************)
-- 
cgit v1.2.3