Some clean-up here and there in dama (coercions removed, implicits added, etc.)

[helm.git] / matita / dama / reals.ma

diff --git a/matita/dama/reals.ma b/matita/dama/reals.ma
index dbd4fa01e26282460a1767a4c27532edded44afc..336bfe2e7c6fb4c084f40c352067fed21eff4940 100644 (file)
--- a/matita/dama/reals.ma
+++ b/matita/dama/reals.ma
@@ -18,7 +18,7 @@ include "ordered_fields_ch0.ma".
 
 record is_real (F:ordered_field_ch0) : Type
 ≝
- { r_archimedean: ∀x:F. ∃n:nat. x ≤ (sum_field F n);
+ { r_archimedean: ∀x:F. ∃n:nat. x ≤ (sum_field ? n);
    r_complete: is_complete F  
  }.
 
@@ -27,7 +27,7 @@ record real: Type \def
    r_real_properties: is_real r_ordered_field_ch0
  }.
 
-definition lim: ∀R:real.∀f:nat→R.is_cauchy_seq R f → R.
+definition lim: ∀R:real.∀f:nat→R.is_cauchy_seq ? f → R.
  intros;
  elim (r_complete ? (r_real_properties R) ? H);
  exact a.
@@ -35,7 +35,7 @@ qed.
 
 definition max_seq: ∀R:real.∀x,y:R. nat → R.
  intros (R x y);
- elim (to_cotransitive R (of_le R) R 0 (inv ? (sum_field R (S n)) ?) (x-y));
+ elim (to_cotransitive R (of_le R) R 0 (inv ? (sum_field ? (S n)) ?) (x-y));
   [ apply x
   | apply not_eq_sum_field_zero ;
     unfold;
@@ -47,7 +47,7 @@ qed.
 
 axiom daemon: False.
 
-theorem cauchy_max_seq: ∀R:real.∀x,y. is_cauchy_seq ? (max_seq R x y).
+theorem cauchy_max_seq: ∀R:real.∀x,y:R. is_cauchy_seq ? (max_seq ? x y).
  intros;
  unfold;
  intros;
@@ -121,4 +121,4 @@ definition max: ∀R:real.R → R → R.
  apply cauchy_max_seq.
 qed.
 
-definition abs \def λR.λx:Type_OF_real R. max R x (-x).
\ No newline at end of file
+definition abs \def λR:real.λx:R. max R x (-x).
\ No newline at end of file