equal
deleted
inserted
replaced
18 primrec of_float :: "float \<Rightarrow> real" where |
18 primrec of_float :: "float \<Rightarrow> real" where |
19 "of_float (Float a b) = real a * pow2 b" |
19 "of_float (Float a b) = real a * pow2 b" |
20 |
20 |
21 defs (overloaded) |
21 defs (overloaded) |
22 real_of_float_def [code_unfold]: "real == of_float" |
22 real_of_float_def [code_unfold]: "real == of_float" |
|
23 |
|
24 declare [[coercion "% x . Float x 0"]] |
|
25 declare [[coercion "real::float\<Rightarrow>real"]] |
23 |
26 |
24 primrec mantissa :: "float \<Rightarrow> int" where |
27 primrec mantissa :: "float \<Rightarrow> int" where |
25 "mantissa (Float a b) = a" |
28 "mantissa (Float a b) = a" |
26 |
29 |
27 primrec scale :: "float \<Rightarrow> int" where |
30 primrec scale :: "float \<Rightarrow> int" where |