Misleading docs for SQL/JSON

Hi,
in docs for SQL/JSON, specifically these examples:
https://www.postgresql.org/docs/devel/functions-json.html#id-1.5.8.22.7.8.6.6

We can find this:

#v+
SELECT JSON_VALUE('"123.45"', '$' RETURNING float);
 json_value
------------
     123.45
(1 row)

SELECT JSON_VALUE('123.45', '$' RETURNING int ERROR ON ERROR);
 json_value
------------
        123
(1 row)

SELECT JSON_VALUE('"03:04 2015-02-01"', '$.datetime("HH24:MI YYYY-MM-DD")' RETURNING date);
 json_value 
------------
 2015-02-01
(1 row)
#v-

The thing is - none of these queries work:

#v+
$ SELECT JSON_VALUE('"123.45"', '$' RETURNING float);
ERROR:  JSON_VALUE() is not yet implemented for json type
LINE 1: SELECT JSON_VALUE('"123.45"', '$' RETURNING float);
               ^

$ SELECT JSON_VALUE('123.45', '$' RETURNING int ERROR ON ERROR);
ERROR:  JSON_VALUE() is not yet implemented for json type
LINE 1: SELECT JSON_VALUE('123.45', '$' RETURNING int ERROR ON ERROR...
               ^

$ SELECT JSON_VALUE('"03:04 2015-02-01"', '$.datetime("HH24:MI YYYY-MM-DD")' RETURNING date);
ERROR:  JSON_VALUE() is not yet implemented for json type
LINE 1: SELECT JSON_VALUE('"03:04 2015-02-01"', '$.datetime("HH24:MI...
               ^
#v-

They do work if I'll cast the item to jsonb, though:

#v+
$ SELECT JSON_VALUE(jsonb '"03:04 2015-02-01"', '$.datetime("HH24:MI YYYY-MM-DD")' RETURNING date);
 json_value 
────────────
 2015-02-01
(1 row)
#v-