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