[definitions] (original) (raw)

See [intro.defs].