The term {tt (float-precision $tau$)} denotes the number of significant digits in the floating point number denoted by $tau$.
(=> (Float-Precision $X $Y) (Nonnegative-Integer $Y))