An instance f of the data type Float is a fixed-precision floating point of size corresponding to double on the machine on which the code is compiled, and is essentially equivalent to the double type. The type of f is FLOAT.
Float is a class derived from the base class Field_element and as such inherits various functions such as print() and type_of().