[isabelle] query about real number representation



Hi, all,

 

I am curious that how Isabelle/HOL represent real number, for example, the positive square root of 2.

 

I know in the theory PReal, it applies Dedekind’s cut to construct positive real numbers from rational numbers.

However, it does not illustrate the way to express explicit real number, for example, the positive square root of 2 in Isabelle/HOL, like the normal floating number, e.g., 3222 * 10^-5 in Isabelle/HOL.

 

Could you kindly enlighten me how Isabelle/HOL specify explicit real numbers?

 

Thanks & Regards

 

Chunqing



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.