SIGNATURE RealConv

-- converting real numbers

IMPORT Nat ONLY nat
       Int ONLY int 
       Real ONLY real 

-- converting to denotations
FUN ` : real -> denotation   -- in exp-format: [-]#.#...#e[+|-]#...#
                             -- max. of 16 digits after point
                             -- trailing zeros are removed unless they
                             -- result from rounding
FUN ` : real ** nat -> denotation 
        -- as above, but with precision given explicitly

FUN `` :real -> denotation  -- in flat format: [-]#...#.#...#
                            -- max. of 16 digits after point
FUN `` :real ** nat -> denotation  
        -- as above, but with precision given explicitly

-- converting to other numeric types
-- both functions truncate argument 

FUN asNat: real -> nat  -- asNat(r) is undefined, if r < 0
FUN asInt: real -> int  

-- old fashioned
FUN trunc: real -> nat