I think it would be better if this invisible doc comments is top-level
doc comments rather than doc comments. Because it is at the start of a
source file. This makes the doc comments visible.