ParseDateTime in src/backend/utils/adt/datetime.c

Hi guys,
https://stackoverflow.com/questions/50153122/how-come-this-postgres-query-is-working
Above guys are surprised by "ignore other punctuation but use as delimiter"
part.
Do you think this should be mentioned in docs?
E.g.
/docs/current/static/functions-formatting.html
docs have very thorough explanation on what is skipped and what parsed.

I believe at least interval '1^minute' equality to interval '1 minute' or
other short comment would make it clear.

Sorry if Iwrote to a wrong list. Maybe I should write to
pgsql-docs(at)lists(dot)postgresql(dot)org instead? please point me If I should.

Regards