[HACKERS] time + date_part oddness?

[Tatsuo Ishii]

I am writing an article of PostgreSQL 7.1 and have some questions.

I can get the millisecond part of a timestamp data using date_part.

test=# SELECT date_part('millisecond','2001/1/15 12:04:05.1234'::TIMESTAMP);
 date_part 
-----------
     123.4
(1 row)

However if I apply the function to a time data, I get a strange result.

test=# SELECT date_part('millisecond','12:04:05.1234'::time);
    date_part     
------------------
 5123.39999999676
(1 row)

Any thought?

(This is current)
--
Tatsuo Ishii