diff options
Diffstat (limited to 'theories/Reals/Raxioms.v')
| -rw-r--r-- | theories/Reals/Raxioms.v | 29 |
1 files changed, 0 insertions, 29 deletions
diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v index e9098104c..7f9db3b18 100644 --- a/theories/Reals/Raxioms.v +++ b/theories/Reals/Raxioms.v @@ -115,35 +115,6 @@ Arguments INR n%nat. (**********************************************************) -(** * Injection from [Z] to [R] *) -(**********************************************************) - -(* compact representation for 2*p *) -Fixpoint IPR_2 (p:positive) : R := - match p with - | xH => 1 + 1 - | xO p => (1 + 1) * IPR_2 p - | xI p => (1 + 1) * (1 + IPR_2 p) - end. - -Definition IPR (p:positive) : R := - match p with - | xH => 1 - | xO p => IPR_2 p - | xI p => 1 + IPR_2 p - end. -Arguments IPR p%positive : simpl never. - -(**********) -Definition IZR (z:Z) : R := - match z with - | Z0 => 0 - | Zpos n => IPR n - | Zneg n => - IPR n - end. -Arguments IZR z%Z : simpl never. - -(**********************************************************) (** * [R] Archimedean *) (**********************************************************) |