diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 60f2d7c0e6..8b07988d02 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -4,6 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich
 -/
 
+/-!
+The formatter turns a `Syntax` tree into a `Format` object, inserting both mandatory whitespace (to separate adjacent
+tokens) as well as "pretty" optional whitespace.
+
+The basic approach works much like the parenthesizer: A right-to-left traversal over the syntax tree and the parser that
+produced it, driven by parser-specific handlers registered via an attribute. The traversal is right-to-left so that when
+emitting a token, we already know the text following it and can decide whether or not whitespace between the two is
+necessary.
+-/
 import Lean.Parser
 import Lean.Meta
 import Lean.Elab.Quotation