times

Concatenates this and other with a space in between.

Equivalent to this + " " + other.

>>> Document("hello") * "world"
hello world

operator fun PrettyPrintable.times(other: String): Document

Convenience method. See plus.