diff --git a/src/data/option/basic.lean b/src/data/option/basic.lean
index 5be65125e8612..e58f906f6cd06 100644
--- a/src/data/option/basic.lean
+++ b/src/data/option/basic.lean
@@ -6,6 +6,30 @@ Authors: Mario Carneiro
 import tactic.basic
 import logic.is_empty
 
+/-!
+# Option of a type
+
+This file develops the basic theory of option types.
+
+If `α` is a type, then `option α` can be understood as the type with one more element than `α`.
+`option α` has terms `some a`, where `a : α`, and `none`, which is the added element.
+This is useful in multiple ways:
+* It is the prototype of addition of terms to a type. See for example `with_bot α` which uses
+  `none` as an element smaller than all others.
+* It can be used to define failsafe partial functions, which return `some the_result_we_expect`
+  if we can find `the_result_we_expect`, and `none` if there is no meaningful result. This forces
+  any subsequent use of the partial function to explicitly deal with the exceptions that make it
+  return `none`.
+* `option` is a monad. We love monads.
+
+`roption` is an alternative to `option` that can be seen as the type of `true`/`false` values
+along with a term `a : α` if the value is `true`.
+
+## Implementation notes
+
+`option` is currently defined in core Lean, but this will change in Lean 4.
+-/
+
 namespace option
 variables {α : Type*} {β : Type*} {γ : Type*}
 
@@ -369,7 +393,7 @@ by cases a; refl
 @[simp] lemma lift_or_get_some_some {f} {a b : α} :
   lift_or_get f (some a) (some b) = f a b := rfl
 
-/-- given an element of `a : option α`, a default element `b : β` and a function `α → β`, apply this
+/-- Given an element of `a : option α`, a default element `b : β` and a function `α → β`, apply this
 function to `a` if it comes from `α`, and return `b` otherwise. -/
 def cases_on' : option α → β → (α → β) → β
 | none     n s := n