set "baseuri" "cic:/matita/CoRN-Decl/reals/CReals".
+include "CoRN.ma".
+
(* $Id: CReals.v,v 1.2 2004/04/05 11:35:38 lcf Exp $ *)
(*#* printing Lim %\ensuremath{\lim}% *)
-(* INCLUDE
-COrdCauchy
-*)
+include "algebra/COrdCauchy.ma".
(*#* * Definition of the notion of reals
The reals are defined as a Cauchy-closed Archimedean constructive
(* Begin_SpecReals *)
-inline cic:/CoRN/reals/CReals/is_CReals.ind.
+inline "cic:/CoRN/reals/CReals/is_CReals.ind".
+
+inline "cic:/CoRN/reals/CReals/CReals.ind".
-inline cic:/CoRN/reals/CReals/CReals.ind.
+coercion cic:/matita/CoRN-Decl/reals/CReals/crl_crr.con 0 (* compounds *).
(* End_SpecReals *)
-inline cic:/CoRN/reals/CReals/Lim.con.
+inline "cic:/CoRN/reals/CReals/Lim.con".
(* UNEXPORTED
Implicit Arguments Lim [IR].