diff --git a/src/Init/Control/Basic.lean b/src/Init/Control/Basic.lean
index 160ee46a22..39d158933a 100644
--- a/src/Init/Control/Basic.lean
+++ b/src/Init/Control/Basic.lean
@@ -270,21 +270,61 @@ Using `control` means that `runInBase` can be used multiple times.
 -/
 
 
-/-- MonadControl is a way of stating that the monad `m` can be 'run inside' the monad `n`.
-
-This is the same as [`MonadBaseControl`](https://hackage.haskell.org/package/monad-control-1.0.3.1/docs/Control-Monad-Trans-Control.html#t:MonadBaseControl) in Haskell.
-To learn about `MonadControl`, see the comment above this docstring.
+/--
+A way to lift a computation from one monad to another while providing the lifted computation with a
+means of interpreting computations from the outer monad. This provides a means of lifting
+higher-order operations automatically.
 
+Clients should typically use `control` or `controlAt`, which request an instance of `MonadControlT`:
+the reflexive, transitive closure of `MonadControl`. New instances should be defined for
+`MonadControl` itself.
 -/
+-- This is the same as
+-- [`MonadBaseControl`](https://hackage.haskell.org/package/monad-control-1.0.3.1/docs/Control-Monad-Trans-Control.html#t:MonadBaseControl)
+-- in Haskell.
 class MonadControl (m : semiOutParam (Type u → Type v)) (n : Type u → Type w) where
+  /--
+  A type that can be used to reconstruct both a returned value and any state used by the outer
+  monad.
+  -/
   stM      : Type u → Type u
+  /--
+  Lifts an action from the inner monad `m` to the outer monad `n`. The inner monad has access to a
+  reverse lifting operator that can run an `n` action, returning a value and state together.
+  -/
   liftWith : {α : Type u} → (({β : Type u} → n β → m (stM β)) → m α) → n α
+  /--
+  Lifts a monadic action that returns a state and a value in the inner monad to an action in the
+  outer monad. The extra state information is used to restore the results of effects from the
+  reverse lift passed to `liftWith`'s parameter.
+  -/
   restoreM : {α : Type u} → m (stM α) → n α
 
-/-- Transitive closure of MonadControl. -/
+/--
+A way to lift a computation from one monad to another while providing the lifted computation with a
+means of interpreting computations from the outer monad. This provides a means of lifting
+higher-order operations automatically.
+
+Clients should typically use `control` or `controlAt`, which request an instance of `MonadControlT`:
+the reflexive, transitive closure of `MonadControl`. New instances should be defined for
+`MonadControl` itself.
+-/
 class MonadControlT (m : Type u → Type v) (n : Type u → Type w) where
+  /--
+  A type that can be used to reconstruct both a returned value and any state used by the outer
+  monad.
+  -/
   stM      : Type u → Type u
+  /--
+  Lifts an action from the inner monad `m` to the outer monad `n`. The inner monad has access to a
+  reverse lifting operator that can run an `n` action, returning a value and state together.
+  -/
   liftWith : {α : Type u} → (({β : Type u} → n β → m (stM β)) → m α) → n α
+  /--
+  Lifts a monadic action that returns a state and a value in the inner monad to an action in the
+  outer monad. The extra state information is used to restore the results of effects from the
+  reverse lift passed to `liftWith`'s parameter.
+  -/
   restoreM {α : Type u} : stM α → n α
 
 export MonadControlT (stM liftWith restoreM)
@@ -300,11 +340,28 @@ instance (m : Type u → Type v) [Pure m] : MonadControlT m m where
   liftWith f := f fun x => x
   restoreM x := pure x
 
+/--
+Lifts an operation from an inner monad to an outer monad, providing it with a reverse lifting
+operator that allows outer monad computations to be run in the inner monad. The lifted operation is
+required to return extra information that is required in order to reconstruct the reverse lift's
+effects in the outer monad; this extra information is determined by `stM`.
+
+This function takes the inner monad as an explicit parameter. Use `control` to infer the monad.
+-/
 @[always_inline, inline]
 def controlAt (m : Type u → Type v) {n : Type u → Type w} [MonadControlT m n] [Bind n] {α : Type u}
     (f : ({β : Type u} → n β → m (stM m n β)) → m (stM m n α)) : n α :=
   liftWith f >>= restoreM
 
+/--
+Lifts an operation from an inner monad to an outer monad, providing it with a reverse lifting
+operator that allows outer monad computations to be run in the inner monad. The lifted operation is
+required to return extra information that is required in order to reconstruct the reverse lift's
+effects in the outer monad; this extra information is determined by `stM`.
+
+This function takes the inner monad as an implicit parameter. Use `controlAt` to specify it
+explicitly.
+-/
 @[always_inline, inline]
 def control {m : Type u → Type v} {n : Type u → Type w} [MonadControlT m n] [Bind n] {α : Type u}
     (f : ({β : Type u} → n β → m (stM m n β)) → m (stM m n α)) : n α :=
diff --git a/src/Init/Control/Option.lean b/src/Init/Control/Option.lean
index 1df47eda77..4f80137b99 100644
--- a/src/Init/Control/Option.lean
+++ b/src/Init/Control/Option.lean
@@ -8,13 +8,22 @@ import Init.Data.Option.Basic
 import Init.Control.Basic
 import Init.Control.Except
 
+set_option linter.missingDocs true
+
 universe u v
 
 instance : ToBool (Option α) := ⟨Option.isSome⟩
 
+/--
+Adds the ability to fail to a monad. Unlike ordinary exceptions, there is no way to signal why a
+failure occurred.
+-/
 def OptionT (m : Type u → Type v) (α : Type u) : Type v :=
   m (Option α)
 
+/--
+Executes an action that might fail in the underlying monad `m`, returning `none` in case of failure.
+-/
 @[always_inline, inline]
 def OptionT.run {m : Type u → Type v} {α : Type u} (x : OptionT m α) : m (Option α) :=
   x
@@ -22,15 +31,25 @@ def OptionT.run {m : Type u → Type v} {α : Type u} (x : OptionT m α) : m (Op
 namespace OptionT
 variable {m : Type u → Type v} [Monad m] {α β : Type u}
 
+/--
+Converts an action that returns an `Option` into one that might fail, with `none` indicating
+failure.
+-/
 protected def mk (x : m (Option α)) : OptionT m α :=
   x
 
+/--
+Sequences two potentially-failing actions. The second action is run only if the first succeeds.
+-/
 @[always_inline, inline]
 protected def bind (x : OptionT m α) (f : α → OptionT m β) : OptionT m β := OptionT.mk do
   match (← x) with
   | some a => f a
   | none   => pure none
 
+/--
+Succeeds with the provided value.
+-/
 @[always_inline, inline]
 protected def pure (a : α) : OptionT m α := OptionT.mk do
   pure (some a)
@@ -40,11 +59,17 @@ instance : Monad (OptionT m) where
   pure := OptionT.pure
   bind := OptionT.bind
 
+/--
+Recovers from failures. Typically used via the `<|>` operator.
+-/
 @[always_inline, inline] protected def orElse (x : OptionT m α) (y : Unit → OptionT m α) : OptionT m α := OptionT.mk do
   match (← x) with
   | some a => pure (some a)
   | _      => y ()
 
+/--
+A recoverable failure.
+-/
 @[always_inline, inline] protected def fail : OptionT m α := OptionT.mk do
   pure none
 
@@ -52,6 +77,12 @@ instance : Alternative (OptionT m) where
   failure := OptionT.fail
   orElse  := OptionT.orElse
 
+/--
+Converts a computation from the underlying monad into one that could fail, even though it does not.
+
+This function is typically implicitly accessed via a `MonadLiftT` instance as part of [automatic
+lifting](lean-manual://section/monad-lifting).
+-/
 @[always_inline, inline] protected def lift (x : m α) : OptionT m α := OptionT.mk do
   return some (← x)
 
@@ -59,6 +90,9 @@ instance : MonadLift m (OptionT m) := ⟨OptionT.lift⟩
 
 instance : MonadFunctor m (OptionT m) := ⟨fun f x => f x⟩
 
+/--
+Handles failures by treating them as exceptions of type `Unit`.
+-/
 @[always_inline, inline] protected def tryCatch (x : OptionT m α) (handle : Unit → OptionT m α) : OptionT m α := OptionT.mk do
   let some a ← x | handle ()
   pure a
diff --git a/src/Init/Control/Reader.lean b/src/Init/Control/Reader.lean
index 541e99d3df..a879cd8ded 100644
--- a/src/Init/Control/Reader.lean
+++ b/src/Init/Control/Reader.lean
@@ -10,12 +10,21 @@ import Init.Control.Basic
 import Init.Control.Id
 import Init.Control.Except
 
+set_option linter.missingDocs true
+
 namespace ReaderT
 
+/--
+Recovers from errors. The same local value is provided to both branches. Typically used via the
+`<|>` operator.
+-/
 @[always_inline, inline]
 protected def orElse [Alternative m] (x₁ : ReaderT ρ m α) (x₂ : Unit → ReaderT ρ m α) : ReaderT ρ m α :=
   fun s => x₁ s <|> x₂ () s
 
+/--
+Fails with a recoverable error.
+-/
 @[always_inline, inline]
 protected def failure [Alternative m] : ReaderT ρ m α :=
   fun _ => failure
@@ -35,4 +44,8 @@ instance : MonadControl m (ReaderT ρ m) where
 instance ReaderT.tryFinally [MonadFinally m] : MonadFinally (ReaderT ρ m) where
   tryFinally' x h ctx := tryFinally' (x ctx) (fun a? => h a? ctx)
 
+/--
+A monad with access to a read-only value of type `ρ`. The value can be locally overridden by
+`withReader`, but it cannot be mutated.
+-/
 @[reducible] def ReaderM (ρ : Type u) := ReaderT ρ Id
diff --git a/src/Init/Control/State.lean b/src/Init/Control/State.lean
index c3e6e60b30..5e91fa6ba4 100644
--- a/src/Init/Control/State.lean
+++ b/src/Init/Control/State.lean
@@ -9,19 +9,42 @@ prelude
 import Init.Control.Basic
 import Init.Control.Id
 import Init.Control.Except
+
+set_option linter.missingDocs true
+
 universe u v w
 
+/--
+Adds a mutable state of type `σ` to a monad.
+
+Actions in the resulting monad are functions that take an initial state and return, in `m`, a tuple
+of a value and a state.
+-/
 def StateT (σ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
   σ → m (α × σ)
 
+/--
+Executes an action from a monad with added state in the underlying monad `m`. Given an initial
+state, it returns a value paired with the final state.
+-/
 @[always_inline, inline]
 def StateT.run {σ : Type u} {m : Type u → Type v} {α : Type u} (x : StateT σ m α) (s : σ) : m (α × σ) :=
   x s
 
+/--
+Executes an action from a monad with added state in the underlying monad `m`. Given an initial
+state, it returns a value, discarding the final state.
+-/
 @[always_inline, inline]
 def StateT.run' {σ : Type u} {m : Type u → Type v} [Functor m] {α : Type u} (x : StateT σ m α) (s : σ) : m α :=
   (·.1) <$> x s
 
+/--
+A tuple-based state monad.
+
+Actions in `StateM σ` are functions that take an initial state and return a value paired with a
+final state.
+-/
 @[reducible]
 def StateM (σ α : Type u) : Type u := StateT σ Id α
 
@@ -38,14 +61,23 @@ section
 variable {σ : Type u} {m : Type u → Type v}
 variable [Monad m] {α β : Type u}
 
+/--
+Returns the given value without modifying the state. Typically used via `Pure.pure`.
+-/
 @[always_inline, inline]
 protected def pure (a : α) : StateT σ m α :=
   fun s => pure (a, s)
 
+/--
+Sequences two actions. Typically used via the `>>=` operator.
+-/
 @[always_inline, inline]
 protected def bind (x : StateT σ m α) (f : α → StateT σ m β) : StateT σ m β :=
   fun s => do let (a, s) ← x s; f a s
 
+/--
+Modifies the value returned by a computation. Typically used via the `<$>` operator.
+-/
 @[always_inline, inline]
 protected def map (f : α → β) (x : StateT σ m α) : StateT σ m β :=
   fun s => do let (a, s) ← x s; pure (f a, s)
@@ -56,10 +88,17 @@ instance : Monad (StateT σ m) where
   bind := StateT.bind
   map  := StateT.map
 
+/--
+Recovers from errors. The state is rolled back on error recovery. Typically used via the `<|>`
+operator.
+-/
 @[always_inline, inline]
 protected def orElse [Alternative m] {α : Type u} (x₁ : StateT σ m α) (x₂ : Unit → StateT σ m α) : StateT σ m α :=
   fun s => x₁ s <|> x₂ () s
 
+/--
+Fails with a recoverable error. The state is rolled back on error recovery.
+-/
 @[always_inline, inline]
 protected def failure [Alternative m] {α : Type u} : StateT σ m α :=
   fun _ => failure
@@ -68,18 +107,40 @@ instance [Alternative m] : Alternative (StateT σ m) where
   failure := StateT.failure
   orElse  := StateT.orElse
 
+/--
+Retrieves the current value of the monad's mutable state.
+
+This increments the reference count of the state, which may inhibit in-place updates.
+-/
 @[always_inline, inline]
 protected def get : StateT σ m σ :=
   fun s => pure (s, s)
 
+/--
+Replaces the mutable state with a new value.
+-/
 @[always_inline, inline]
 protected def set : σ → StateT σ m PUnit :=
   fun s' _ => pure (⟨⟩, s')
 
+/--
+Applies a function to the current state that both computes a new state and a value. The new state
+replaces the current state, and the value is returned.
+
+It is equivalent to `do let (a, s) := f (← StateT.get); StateT.set s; pure a`. However, using
+`StateT.modifyGet` may lead to better performance because it doesn't add a new reference to the
+state value, and additional references can inhibit in-place updates of data.
+-/
 @[always_inline, inline]
 protected def modifyGet (f : σ → α × σ) : StateT σ m α :=
   fun s => pure (f s)
 
+/--
+Runs an action from the underlying monad in the monad with state. The state is not modified.
+
+This function is typically implicitly accessed via a `MonadLiftT` instance as part of [automatic
+lifting](lean-manual://section/monad-lifting).
+-/
 @[always_inline, inline]
 protected def lift {α : Type u} (t : m α) : StateT σ m α :=
   fun s => do let a ← t; pure (a, s)
diff --git a/src/Init/Control/StateCps.lean b/src/Init/Control/StateCps.lean
index 94449123c2..88229328d5 100644
--- a/src/Init/Control/StateCps.lean
+++ b/src/Init/Control/StateCps.lean
@@ -6,24 +6,45 @@ Authors: Leonardo de Moura
 prelude
 import Init.Control.Lawful.Basic
 
+set_option linter.missingDocs true
+
 /-!
 The State monad transformer using CPS style.
 -/
 
+/--
+An alternative implementation of a state monad transformer that internally uses continuation passing
+style instead of tuples.
+-/
 def StateCpsT (σ : Type u) (m : Type u → Type v) (α : Type u) := (δ : Type u) → σ → (α → σ → m δ) → m δ
 
 namespace StateCpsT
 
 variable {α σ : Type u} {m : Type u → Type v}
 
+/--
+Runs a stateful computation that's represented using continuation passing style by providing it with
+an initial state and a continuation.
+-/
 @[always_inline, inline]
 def runK (x : StateCpsT σ m α) (s : σ) (k : α → σ → m β) : m β :=
   x _ s k
 
+/--
+Executes an action from a monad with added state in the underlying monad `m`. Given an initial
+state, it returns a value paired with the final state.
+
+While the state is internally represented in continuation passing style, the resulting value is the
+same as for a non-CPS state monad.
+-/
 @[always_inline, inline]
 def run [Monad m] (x : StateCpsT σ m α) (s : σ) : m (α × σ) :=
   runK x s (fun a s => pure (a, s))
 
+/--
+Executes an action from a monad with added state in the underlying monad `m`. Given an initial
+state, it returns a value, discarding the final state.
+-/
 @[always_inline, inline]
 def run' [Monad m] (x : StateCpsT σ m α) (s : σ) : m α :=
   runK x s (fun a _ => pure a)
@@ -43,6 +64,12 @@ instance : MonadStateOf σ (StateCpsT σ m) where
   set s := fun _ _ k => k ⟨⟩ s
   modifyGet f := fun _ s k => let (a, s) := f s; k a s
 
+/--
+Runs an action from the underlying monad in the monad with state. The state is not modified.
+
+This function is typically implicitly accessed via a `MonadLiftT` instance as part of [automatic
+lifting](lean-manual://section/monad-lifting).
+-/
 @[always_inline, inline]
 protected def lift [Monad m] (x : m α) : StateCpsT σ m α :=
   fun _ s k => x >>= (k . s)
diff --git a/src/Init/Control/StateRef.lean b/src/Init/Control/StateRef.lean
index 6aa41d8c27..7ed4edabf3 100644
--- a/src/Init/Control/StateRef.lean
+++ b/src/Init/Control/StateRef.lean
@@ -8,10 +8,23 @@ The State monad transformer using IO references.
 prelude
 import Init.System.ST
 
+set_option linter.missingDocs true
+
+/--
+A state monad that uses an actual mutable reference cell (i.e. an `ST.Ref ω σ`).
+
+The macro `StateRefT σ m α` infers `ω` from `m`. It should normally be used instead.
+-/
 def StateRefT' (ω : Type) (σ : Type) (m : Type → Type) (α : Type) : Type := ReaderT (ST.Ref ω σ) m α
 
 /-! Recall that `StateRefT` is a macro that infers `ω` from the `m`. -/
 
+/--
+Executes an action from a monad with added state in the underlying monad `m`. Given an initial
+state, it returns a value paired with the final state.
+
+The monad `m` must support `ST` effects in order to create and mutate reference cells.
+-/
 @[always_inline, inline]
 def StateRefT'.run {ω σ : Type} {m : Type → Type} [Monad m] [MonadLiftT (ST ω) m] {α : Type} (x : StateRefT' ω σ m α) (s : σ) : m (α × σ) := do
   let ref ← ST.mkRef s
@@ -19,6 +32,12 @@ def StateRefT'.run {ω σ : Type} {m : Type → Type} [Monad m] [MonadLiftT (ST
   let s ← ref.get
   pure (a, s)
 
+/--
+Executes an action from a monad with added state in the underlying monad `m`. Given an initial
+state, it returns a value, discarding the final state.
+
+The monad `m` must support `ST` effects in order to create and mutate reference cells.
+-/
 @[always_inline, inline]
 def StateRefT'.run' {ω σ : Type} {m : Type → Type} [Monad m] [MonadLiftT (ST ω) m] {α : Type} (x : StateRefT' ω σ m α) (s : σ) : m α := do
   let (a, _) ← x.run s
@@ -27,6 +46,12 @@ def StateRefT'.run' {ω σ : Type} {m : Type → Type} [Monad m] [MonadLiftT (ST
 namespace StateRefT'
 variable {ω σ : Type} {m : Type → Type} {α : Type}
 
+/--
+Runs an action from the underlying monad in the monad with state. The state is not modified.
+
+This function is typically implicitly accessed via a `MonadLiftT` instance as part of [automatic
+lifting](lean-manual://section/monad-lifting).
+-/
 @[always_inline, inline]
 protected def lift (x : m α) : StateRefT' ω σ m α :=
   fun _ => x
@@ -36,14 +61,30 @@ instance : MonadLift m (StateRefT' ω σ m) := ⟨StateRefT'.lift⟩
 instance (σ m) : MonadFunctor m (StateRefT' ω σ m) := inferInstanceAs (MonadFunctor m (ReaderT _ _))
 instance [Alternative m] [Monad m] : Alternative (StateRefT' ω σ m) := inferInstanceAs (Alternative (ReaderT _ _))
 
+/--
+Retrieves the current value of the monad's mutable state.
+
+This increments the reference count of the state, which may inhibit in-place updates.
+-/
 @[inline]
 protected def get [MonadLiftT (ST ω) m] : StateRefT' ω σ m σ :=
   fun ref => ref.get
 
+/--
+Replaces the mutable state with a new value.
+-/
 @[inline]
 protected def set [MonadLiftT (ST ω) m] (s : σ) : StateRefT' ω σ m PUnit :=
   fun ref => ref.set s
 
+/--
+Applies a function to the current state that both computes a new state and a value. The new state
+replaces the current state, and the value is returned.
+
+It is equivalent to a `get` followed by a `set`. However, using `modifyGet` may lead to higher
+performance because it doesn't add a new reference to the state value. Additional references can
+inhibit in-place updates of data.
+-/
 @[inline]
 protected def modifyGet [MonadLiftT (ST ω) m] (f : σ → α × σ) : StateRefT' ω σ m α :=
   fun ref => ref.modifyGet f
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 16e4d424b4..369e1b074f 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -3175,31 +3175,46 @@ instance [Monad m] : [Nonempty α] → Nonempty (m α)
   | ⟨x⟩ => ⟨pure x⟩
 
 /--
-A function for lifting a computation from an inner `Monad` to an outer `Monad`.
-Like Haskell's [`MonadTrans`], but `n` does not have to be a monad transformer.
-Alternatively, an implementation of [`MonadLayer`] without `layerInvmap` (so far).
+Computations in the monad `m` can be run in the monad `n`. These translations are inserted
+automatically by the compiler.
 
-  [`MonadTrans`]: https://hackage.haskell.org/package/transformers-0.5.5.0/docs/Control-Monad-Trans-Class.html
-  [`MonadLayer`]: https://hackage.haskell.org/package/layers-0.1/docs/Control-Monad-Layer.html#t:MonadLayer
+Usually, `n` consists of some number of monad transformers applied to `m`, but this is not
+mandatory.
+
+New instances should use this class, `MonadLift`. Clients that require one monad to be liftable into
+another should instead request `MonadLiftT`, which is the reflexive, transitive closure of
+`MonadLift`.
 -/
+-- Like Haskell's [`MonadTrans`], but `n` does not have to be a monad transformer.
+-- Alternatively, an implementation of [`MonadLayer`] without `layerInvmap` (so far).
+
+--   [`MonadTrans`]: https://hackage.haskell.org/package/transformers-0.5.5.0/docs/Control-Monad-Trans-Class.html
+--   [`MonadLayer`]: https://hackage.haskell.org/package/layers-0.1/docs/Control-Monad-Layer.html#t:MonadLayer
 class MonadLift (m : semiOutParam (Type u → Type v)) (n : Type u → Type w) where
-  /-- Lifts a value from monad `m` into monad `n`. -/
+  /-- Translates an action from monad `m` into monad `n`. -/
   monadLift : {α : Type u} → m α → n α
 
 /--
-The reflexive-transitive closure of `MonadLift`. `monadLift` is used to
-transitively lift monadic computations such as `StateT.get` or `StateT.put s`.
-Corresponds to Haskell's [`MonadLift`].
+Computations in the monad `m` can be run in the monad `n`. These translations are inserted
+automatically by the compiler.
 
-  [`MonadLift`]: https://hackage.haskell.org/package/layers-0.1/docs/Control-Monad-Layer.html#t:MonadLift
+Usually, `n` consists of some number of monad transformers applied to `m`, but this is not
+mandatory.
+
+This is the reflexive, transitive closure of `MonadLift`. Clients that require one monad to be
+liftable into another should request an instance of `MonadLiftT`. New instances should instead be
+defined for `MonadLift` itself.
 -/
+-- Corresponds to Haskell's [`MonadLift`].
+--
+--   [`MonadLift`]: https://hackage.haskell.org/package/layers-0.1/docs/Control-Monad-Layer.html#t:MonadLift
 class MonadLiftT (m : Type u → Type v) (n : Type u → Type w) where
-  /-- Lifts a value from monad `m` into monad `n`. -/
+  /-- Translates an action from monad `m` into monad `n`. -/
   monadLift : {α : Type u} → m α → n α
 
 export MonadLiftT (monadLift)
 
-/-- Lifts a value from monad `m` into monad `n`. -/
+@[inherit_doc monadLift]
 abbrev liftM := @monadLift
 
 @[always_inline]
@@ -3236,23 +3251,36 @@ instance (m) : MonadEvalT m m where
   monadEval x := x
 
 /--
-A functor in the category of monads. Can be used to lift monad-transforming functions.
-Based on [`MFunctor`] from the `pipes` Haskell package, but not restricted to
-monad transformers. Alternatively, an implementation of [`MonadTransFunctor`].
+A way to interpret a fully-polymorphic function in `m` into `n`. Such a function can be thought of
+as one that may change the effects in `m`, but can't do so based on specific values that are
+provided.
 
-  [`MFunctor`]: https://hackage.haskell.org/package/pipes-2.4.0/docs/Control-MFunctor.html
-  [`MonadTransFunctor`]: http://duairc.netsoc.ie/layers-docs/Control-Monad-Layer.html#t:MonadTransFunctor
+Clients of `MonadFunctor` should typically use `MonadFunctorT`, which is the reflexive, transitive
+closure of `MonadFunctor`. New instances should be defined for `MonadFunctor.`
 -/
+-- Based on [`MFunctor`] from the `pipes` Haskell package, but not restricted to
+-- monad transformers. Alternatively, an implementation of [`MonadTransFunctor`].
+--   [`MFunctor`]: https://hackage.haskell.org/package/pipes-2.4.0/docs/Control-MFunctor.html
+--   [`MonadTransFunctor`]: http://duairc.netsoc.ie/layers-docs/Control-Monad-Layer.html#t:MonadTransFunctor
 class MonadFunctor (m : semiOutParam (Type u → Type v)) (n : Type u → Type w) where
-  /-- Lifts a monad morphism `f : {β : Type u} → m β → m β` to
-  `monadMap f : {α : Type u} → n α → n α`. -/
+  /--
+  Lifts a fully-polymorphic transformation of `m` into `n`.
+  -/
   monadMap {α : Type u} : ({β : Type u} → m β → m β) → n α → n α
 
-/-- The reflexive-transitive closure of `MonadFunctor`.
-`monadMap` is used to transitively lift `Monad` morphisms. -/
+/--
+A way to interpret a fully-polymorphic function in `m` into `n`. Such a function can be thought of
+as one that may change the effects in `m`, but can't do so based on specific values that are
+provided.
+
+This is the reflexive, transitive closure of `MonadFunctor`. It automatically chains together
+`MonadFunctor` instances as needed. Clients of `MonadFunctor` should typically use `MonadFunctorT`,
+but new instances should be defined for `MonadFunctor`.
+-/
 class MonadFunctorT (m : Type u → Type v) (n : Type u → Type w) where
-  /-- Lifts a monad morphism `f : {β : Type u} → m β → m β` to
-  `monadMap f : {α : Type u} → n α → n α`. -/
+  /--
+  Lifts a fully-polymorphic transformation of `m` into `n`.
+  -/
   monadMap {α : Type u} : ({β : Type u} → m β → m β) → n α → n α
 
 export MonadFunctorT (monadMap)
@@ -3331,7 +3359,7 @@ handlers do not have exception type annotations.
 -/
 class MonadExcept (ε : outParam (Type u)) (m : Type v → Type w) where
   /--
-  Throws an exception of type `ε` to the nearest enclosing `catch`.
+  Throws an exception of type `ε` to the nearest enclosing handler.
   -/
   throw {α : Type v} : ε → m α
   /--
@@ -3371,10 +3399,11 @@ instance [MonadExcept ε m] {α : Type v} : OrElse (m α) where
 end MonadExcept
 
 /--
-An implementation of Haskell's [`ReaderT`]. This is a monad transformer which
-equips a monad with additional read-only state, of type `ρ`.
+Adds the ability to access a read-only value of type `ρ` to a monad. The value can be locally
+overridden by `withReader`, but it cannot be mutated.
 
-  [`ReaderT`]: https://hackage.haskell.org/package/transformers-0.5.5.0/docs/Control-Monad-Trans-Reader.html#t:ReaderT
+Actions in the resulting monad are functions that take the local value as a parameter, returning
+ordinary actions in `m`.
 -/
 def ReaderT (ρ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
   ρ → m α
@@ -3383,8 +3412,7 @@ instance (ρ : Type u) (m : Type u → Type v) (α : Type u) [Inhabited (m α)]
   default := fun _ => default
 
 /--
-If `x : ReaderT ρ m α` and `r : ρ`, then `x.run r : ρ` runs the monad with the
-given reader state.
+Executes an action from a monad with a read-only value in the underlying monad `m`.
 -/
 @[always_inline, inline]
 def ReaderT.run {ρ : Type u} {m : Type u → Type v} {α : Type u} (x : ReaderT ρ m α) (r : ρ) : m α :=
@@ -3408,17 +3436,26 @@ end
 section
 variable {ρ : Type u} {m : Type u → Type v}
 
-/-- `(← read) : ρ` gets the read-only state of a `ReaderT ρ`. -/
+/--
+Retrieves the reader monad's local value. Typically accessed via `read`, or via `readThe` when more
+than one local value is available.
+-/
 @[always_inline, inline]
 protected def read [Monad m] : ReaderT ρ m ρ :=
   pure
 
-/-- The `pure` operation of the `ReaderT` monad. -/
+/--
+Returns the provided value `a`, ignoring the reader monad's local value. Typically used via
+`Pure.pure`.
+-/
 @[always_inline, inline]
 protected def pure [Monad m] {α} (a : α) : ReaderT ρ m α :=
   fun _ => pure a
 
-/-- The `bind` operation of the `ReaderT` monad. -/
+/--
+Sequences two reader monad computations. Both are provided with the local value, and the second is
+passed the value of the first. Typically used via the `>>=` operator.
+-/
 @[always_inline, inline]
 protected def bind [Monad m] {α β} (x : ReaderT ρ m α) (f : α → ReaderT ρ m β) : ReaderT ρ m β :=
   fun r => bind (x r) fun a => f a r
@@ -3442,8 +3479,8 @@ instance (ρ m) : MonadFunctor m (ReaderT ρ m) where
   monadMap f x := fun ctx => f (x ctx)
 
 /--
-`adapt (f : ρ' → ρ)` precomposes function `f` on the reader state of a
-`ReaderT ρ`, yielding a `ReaderT ρ'`.
+Modifies a reader monad's local value with `f`. The resulting computation applies `f` to the
+incoming local value and passes the result to the inner computation.
 -/
 @[always_inline, inline]
 protected def adapt {ρ' α : Type u} (f : ρ' → ρ) : ReaderT ρ m α → ReaderT ρ' m α :=
@@ -3453,38 +3490,50 @@ end
 end ReaderT
 
 /--
-An implementation of Haskell's [`MonadReader`] (sans functional dependency; see also `MonadReader`
-in this module). It does not contain `local` because this
-function cannot be lifted using `monadLift`. `local` is instead provided by
-the `MonadWithReader` class as `withReader`.
+Reader monads provide the ability to implicitly thread a value through a computation. The value can
+be read, but not written. A `MonadWithReader ρ` instance additionally allows the value to be locally
+overridden for a sub-computation.
 
-Note: This class can be seen as a simplification of the more "principled" definition
-```
-class MonadReaderOf (ρ : Type u) (n : Type u → Type u) where
-  lift {α : Type u} : ({m : Type u → Type u} → [Monad m] → ReaderT ρ m α) → n α
-```
-
-  [`MonadReader`]: https://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-Reader-Class.html#t:MonadReader
+In this class, `ρ` is a `semiOutParam`, which means that it can influence the choice of instance.
+`MonadReader ρ` provides the same operations, but requires that `ρ` be inferrable from `m`.
 -/
+-- Note: This class can be seen as a simplification of the more "principled" definition
+-- ```
+-- class MonadReaderOf (ρ : Type u) (n : Type u → Type u) where
+--   lift {α : Type u} : ({m : Type u → Type u} → [Monad m] → ReaderT ρ m α) → n α
+-- ```
 class MonadReaderOf (ρ : semiOutParam (Type u)) (m : Type u → Type v) where
-  /-- `(← read) : ρ` reads the state out of monad `m`. -/
+  /-- Retrieves the local value. -/
   read : m ρ
 
 /--
-Like `read`, but with `ρ` explicit. This is useful if a monad supports
-`MonadReaderOf` for multiple different types `ρ`.
+Reader monads provide the ability to implicitly thread a value through a computation. The value can
+be read, but not written. A `MonadWithReader ρ` instance additionally allows the value to be locally
+overridden for a sub-computation.
+
+In this class, `ρ` is an `outParam`, which means that it is inferred from `m`. `MonadReaderOf ρ`
+provides the same operations, but allows `ρ` to influence instance synthesis.
+-/
+class MonadReader (ρ : outParam (Type u)) (m : Type u → Type v) where
+  /--
+  Retrieves the local value.
+
+  Use `readThe` to explicitly specify a type when more than one value is available.
+  -/
+  read : m ρ
+
+export MonadReader (read)
+
+/--
+Retrieves the local value whose type is `ρ`.  This is useful when a monad supports reading more that
+one type of value.
+
+Use `read` for a version that expects the type `ρ` to be inferred from `m`.
 -/
 @[always_inline, inline]
 def readThe (ρ : Type u) {m : Type u → Type v} [MonadReaderOf ρ m] : m ρ :=
   MonadReaderOf.read
 
-/-- Similar to `MonadReaderOf`, but `ρ` is an `outParam` for convenience. -/
-class MonadReader (ρ : outParam (Type u)) (m : Type u → Type v) where
-  /-- `(← read) : ρ` reads the state out of monad `m`. -/
-  read : m ρ
-
-export MonadReader (read)
-
 instance (ρ : Type u) (m : Type u → Type v) [MonadReaderOf ρ m] : MonadReader ρ m where
   read := readThe ρ
 
@@ -3495,29 +3544,47 @@ instance {ρ : Type u} {m : Type u → Type v} [Monad m] : MonadReaderOf ρ (Rea
   read := ReaderT.read
 
 /--
-`MonadWithReaderOf ρ` adds the operation `withReader : (ρ → ρ) → m α → m α`.
-This runs the inner `x : m α` inside a modified context after applying the
-function `f : ρ → ρ`. In addition to `ReaderT` itself, this operation lifts
-over most monad transformers, so it allows us to apply `withReader` to monads
-deeper in the stack.
+A reader monad that additionally allows the value to be locally overridden.
+
+In this class, `ρ` is a `semiOutParam`, which means that it can influence the choice of instance.
+`MonadWithReader ρ` provides the same operations, but requires that `ρ` be inferrable from `m`.
 -/
 class MonadWithReaderOf (ρ : semiOutParam (Type u)) (m : Type u → Type v) where
-  /-- `withReader (f : ρ → ρ) (x : m α) : m α`  runs the inner `x : m α` inside
-  a modified context after applying the function `f : ρ → ρ`.-/
-  withReader {α : Type u} : (ρ → ρ) → m α → m α
+  /--
+  Locally modifies the reader monad's value while running an action.
+
+  During the inner action `x`, reading the value returns `f` applied to the original value. After
+  control returns from `x`, the reader monad's value is restored.
+  -/
+  withReader {α : Type u} (f : ρ → ρ) (x : m α) : m α
 
 /--
-Like `withReader`, but with `ρ` explicit. This is useful if a monad supports
-`MonadWithReaderOf` for multiple different types `ρ`.
+Locally modifies the reader monad's value while running an action, with the reader monad's local
+value type specified explicitly. This is useful when a monad supports reading more than one type of
+value.
+
+During the inner action `x`, reading the value returns `f` applied to the original value. After
+control returns from `x`, the reader monad's value is restored.
+
+Use `withReader` for a version that expects the local value's type to be inferred from `m`.
 -/
 @[always_inline, inline]
 def withTheReader (ρ : Type u) {m : Type u → Type v} [MonadWithReaderOf ρ m] {α : Type u} (f : ρ → ρ) (x : m α) : m α :=
   MonadWithReaderOf.withReader f x
 
-/-- Similar to `MonadWithReaderOf`, but `ρ` is an `outParam` for convenience. -/
+/--
+A reader monad that additionally allows the value to be locally overridden.
+
+In this class, `ρ` is an `outParam`, which means that it is inferred from `m`. `MonadWithReaderOf ρ`
+provides the same operations, but allows `ρ` to influence instance synthesis.
+-/
 class MonadWithReader (ρ : outParam (Type u)) (m : Type u → Type v) where
-  /-- `withReader (f : ρ → ρ) (x : m α) : m α`  runs the inner `x : m α` inside
-  a modified context after applying the function `f : ρ → ρ`.-/
+  /--
+  Locally modifies the reader monad's value while running an action.
+
+  During the inner action `x`, reading the value returns `f` applied to the original value. After
+  control returns from `x`, the reader monad's value is restored.
+  -/
   withReader {α : Type u} : (ρ → ρ) → m α → m α
 
 export MonadWithReader (withReader)
@@ -3532,61 +3599,98 @@ instance {ρ : Type u} {m : Type u → Type v} : MonadWithReaderOf ρ (ReaderT 
   withReader f x := fun ctx => x (f ctx)
 
 /--
-An implementation of [`MonadState`]. In contrast to the Haskell implementation,
-we use overlapping instances to derive instances automatically from `monadLift`.
+State monads provide a value of a given type (the _state_) that can be retrieved or replaced.
+Instances may implement these operations by passing state values around, by using a mutable
+reference cell (e.g. `ST.Ref σ`), or in other ways.
 
-  [`MonadState`]: https://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-State-Class.html
+In this class, `σ` is a `semiOutParam`, which means that it can influence the choice of instance.
+`MonadState σ` provides the same operations, but requires that `σ` be inferrable from `m`.
+
+The mutable state of a state monad is visible between multiple `do`-blocks or functions, unlike
+[local mutable state](lean-manual://section/do-notation-let-mut) in `do`-notation.
 -/
 class MonadStateOf (σ : semiOutParam (Type u)) (m : Type u → Type v) where
-  /-- `(← get) : σ` gets the state out of a monad `m`. -/
+  /--
+  Retrieves the current value of the monad's mutable state.
+  -/
   get : m σ
-  /-- `set (s : σ)` replaces the state with value `s`. -/
+  /--
+  Replaces the current value of the mutable state with a new one.
+  -/
   set : σ → m PUnit
-  /-- `modifyGet (f : σ → α × σ)` applies `f` to the current state, replaces
-  the state with the return value, and returns a computed value.
+  /--
+  Applies a function to the current state that both computes a new state and a value. The new state
+  replaces the current state, and the value is returned.
 
-  It is equivalent to `do let (a, s) := f (← get); put s; pure a`, but
-  `modifyGet f` may be preferable because the former does not use the state
-  linearly (without sufficient inlining). -/
+  It is equivalent to `do let (a, s) := f (← get); set s; pure a`. However, using `modifyGet` may
+  lead to higher performance because it doesn't add a new reference to the state value. Additional
+  references can inhibit in-place updates of data.
+  -/
   modifyGet {α : Type u} : (σ → Prod α σ) → m α
 
 export MonadStateOf (set)
 
 /--
-Like `get`, but with `σ` explicit. This is useful if a monad supports
-`MonadStateOf` for multiple different types `σ`.
+Gets the current state that has the explicitly-provided type `σ`. When the current monad has
+multiple state types available, this function selects one of them.
 -/
 abbrev getThe (σ : Type u) {m : Type u → Type v} [MonadStateOf σ m] : m σ :=
   MonadStateOf.get
 
 /--
-Like `modify`, but with `σ` explicit. This is useful if a monad supports
-`MonadStateOf` for multiple different types `σ`.
+Mutates the current state that has the explicitly-provided type `σ`, replacing its value with the
+result of applying `f` to it. When the current monad has multiple state types available, this
+function selects one of them.
+
+It is equivalent to `do set (f (← get))`. However, using `modify` may lead to higher performance
+because it doesn't add a new reference to the state value. Additional references can inhibit
+in-place updates of data.
 -/
 @[always_inline, inline]
 abbrev modifyThe (σ : Type u) {m : Type u → Type v} [MonadStateOf σ m] (f : σ → σ) : m PUnit :=
   MonadStateOf.modifyGet fun s => (PUnit.unit, f s)
 
 /--
-Like `modifyGet`, but with `σ` explicit. This is useful if a monad supports
-`MonadStateOf` for multiple different types `σ`.
+Applies a function to the current state that has the explicitly-provided type `σ`. The function both
+computes a new state and a value. The new state replaces the current state, and the value is
+returned.
+
+It is equivalent to `do let (a, s) := f (← getThe σ); set s; pure a`. However, using `modifyGetThe`
+may lead to higher performance because it doesn't add a new reference to the state value. Additional
+references can inhibit in-place updates of data.
 -/
 @[always_inline, inline]
 abbrev modifyGetThe {α : Type u} (σ : Type u) {m : Type u → Type v} [MonadStateOf σ m] (f : σ → Prod α σ) : m α :=
   MonadStateOf.modifyGet f
 
-/-- Similar to `MonadStateOf`, but `σ` is an `outParam` for convenience. -/
-class MonadState (σ : outParam (Type u)) (m : Type u → Type v) where
-  /-- `(← get) : σ` gets the state out of a monad `m`. -/
-  get : m σ
-  /-- `set (s : σ)` replaces the state with value `s`. -/
-  set : σ → m PUnit
-  /-- `modifyGet (f : σ → α × σ)` applies `f` to the current state, replaces
-  the state with the return value, and returns a computed value.
+/--
+State monads provide a value of a given type (the _state_) that can be retrieved or replaced.
+Instances may implement these operations by passing state values around, by using a mutable
+reference cell (e.g. `ST.Ref σ`), or in other ways.
 
-  It is equivalent to `do let (a, s) := f (← get); put s; pure a`, but
-  `modifyGet f` may be preferable because the former does not use the state
-  linearly (without sufficient inlining). -/
+In this class, `σ` is an `outParam`, which means that it is inferred from `m`. `MonadStateOf σ`
+provides the same operations, but allows `σ` to influence instance synthesis.
+
+The mutable state of a state monad is visible between multiple `do`-blocks or functions, unlike
+[local mutable state](lean-manual://section/do-notation-let-mut) in `do`-notation.
+-/
+class MonadState (σ : outParam (Type u)) (m : Type u → Type v) where
+  /--
+  Retrieves the current value of the monad's mutable state.
+  -/
+  get : m σ
+  /--
+  Replaces the current value of the mutable state with a new one.
+  -/
+  set : σ → m PUnit
+  /--
+  Applies a function to the current state that both computes a new state and a value. The new state
+  replaces the current state, and the value is returned.
+
+  It is equivalent to `do let (a, s) := f (← get); set s; pure a`. However, using `modifyGet` may
+  lead to higher performance because it doesn't add a new reference to the state value. Additional
+  references can inhibit in-place updates of data.
+  -/
   modifyGet {α : Type u} : (σ → Prod α σ) → m α
 
 export MonadState (get modifyGet)
@@ -3597,18 +3701,22 @@ instance (σ : Type u) (m : Type u → Type v) [MonadStateOf σ m] : MonadState
   modifyGet f := MonadStateOf.modifyGet f
 
 /--
-`modify (f : σ → σ)` applies the function `f` to the state.
+Mutates the current state, replacing its value with the result of applying `f` to it.
 
-It is equivalent to `do set (f (← get))`, but `modify f` may be preferable
-because the former does not use the state linearly (without sufficient inlining).
+Use `modifyThe` to explicitly select a state type to modify.
+
+It is equivalent to `do set (f (← get))`. However, using `modify` may lead to higher performance
+because it doesn't add a new reference to the state value. Additional references can inhibit
+in-place updates of data.
 -/
 @[always_inline, inline]
 def modify {σ : Type u} {m : Type u → Type v} [MonadState σ m] (f : σ → σ) : m PUnit :=
   modifyGet fun s => (PUnit.unit, f s)
 
 /--
-`getModify f` gets the state, applies function `f`, and returns the old value
-of the state. It is equivalent to `get <* modify f` but may be more efficient.
+Replaces the state with the result of applying `f` to it. Returns the old value of the state.
+
+It is equivalent to `get <* modify f` but may be more efficient.
 -/
 @[always_inline, inline]
 def getModify {σ : Type u} {m : Type u → Type v} [MonadState σ m] (f : σ → σ) : m σ :=
@@ -3625,13 +3733,16 @@ instance {σ : Type u} {m : Type u → Type v} {n : Type u → Type w} [MonadLif
 namespace EStateM
 
 /--
-`Result ε σ α` is equivalent to `Except ε α × σ`, but using a single
-combined inductive yields a more efficient data representation.
+The value returned from a combined state and exception monad in which exceptions do not
+automatically roll back the state.
+
+`Result ε σ α` is equivalent to `Except ε α × σ`, but using a single combined inductive type yields
+a more efficient data representation.
 -/
 inductive Result (ε σ α : Type u) where
-  /-- A success value of type `α`, and a new state `σ`. -/
+  /-- A success value of type `α` and a new state `σ`. -/
   | ok    : α → σ → Result ε σ α
-  /-- A failure value of type `ε`, and a new state `σ`. -/
+  /-- An exception of type `ε` and a new state `σ`. -/
   | error : ε → σ → Result ε σ α
 
 variable {ε σ α : Type u}
@@ -3643,8 +3754,11 @@ end EStateM
 
 open EStateM (Result) in
 /--
-`EStateM ε σ` is a combined error and state monad, equivalent to
-`ExceptT ε (StateM σ)` but more efficient.
+A combined state and exception monad in which exceptions do not automatically roll back the state.
+
+Instances of `EStateM.Backtrackable` provide a way to roll back some part of the state if needed.
+
+`EStateM ε σ` is equivalent to `ExceptT ε (StateM σ)`, but it is more efficient.
 -/
 def EStateM (ε σ α : Type u) := σ → Result ε σ α
 
@@ -3655,45 +3769,53 @@ variable {ε σ α β : Type u}
 instance [Inhabited ε] : Inhabited (EStateM ε σ α) where
   default := fun s => Result.error default s
 
-/-- The `pure` operation of the `EStateM` monad. -/
+/--
+Returns a value without modifying the state or throwing an exception.
+-/
 @[always_inline, inline]
 protected def pure (a : α) : EStateM ε σ α := fun s =>
   Result.ok a s
 
-/-- The `set` operation of the `EStateM` monad. -/
-@[always_inline, inline]
+@[always_inline, inline, inherit_doc MonadState.set]
 protected def set (s : σ) : EStateM ε σ PUnit := fun _ =>
   Result.ok ⟨⟩ s
 
-/-- The `get` operation of the `EStateM` monad. -/
-@[always_inline, inline]
+@[always_inline, inline, inherit_doc MonadState.get]
 protected def get : EStateM ε σ σ := fun s =>
   Result.ok s s
 
-/-- The `modifyGet` operation of the `EStateM` monad. -/
-@[always_inline, inline]
+@[always_inline, inline, inherit_doc MonadState.modifyGet]
 protected def modifyGet (f : σ → Prod α σ) : EStateM ε σ α := fun s =>
   match f s with
   | (a, s) => Result.ok a s
 
-/-- The `throw` operation of the `EStateM` monad. -/
-@[always_inline, inline]
+@[always_inline, inline, inherit_doc MonadExcept.throw]
 protected def throw (e : ε) : EStateM ε σ α := fun s =>
   Result.error e s
 
 /--
-Auxiliary instance for saving/restoring the "backtrackable" part of the state.
-Here `σ` is the state, and `δ` is some subpart of it, and we have a
-getter and setter for it (a "lens" in the Haskell terminology).
+Exception handlers in `EStateM` save some part of the state, determined by `δ`, and restore it if an
+exception is caught. By default, `δ` is `Unit`, and no information is saved.
 -/
 class Backtrackable (δ : outParam (Type u)) (σ : Type u) where
-  /-- `save s : δ` retrieves a copy of the backtracking state out of the state. -/
+  /--
+  Extracts the information in the state that should be rolled back if an exception is handled.
+  -/
   save    : σ → δ
-  /-- `restore (s : σ) (x : δ) : σ` applies the old backtracking state `x` to
-  the state `s` to get a backtracked state `s'`. -/
+  /--
+  Updates the current state with the saved information that should be rolled back. This updated
+  state becomes the current state when an exception is handled.
+  -/
   restore : σ → δ → σ
 
-/-- Implementation of `tryCatch` for `EStateM` where the state is `Backtrackable`. -/
+/--
+Handles exceptions thrown in the combined error and state monad.
+
+The `Backtrackable δ σ` instance is used to save a snapshot of part of the state prior to running
+`x`. If an exception is caught, the state is updated with the saved snapshot, rolling back part of
+the state. If no instance of `Backtrackable` is provided, a fallback instance in which `δ` is `Unit`
+is used, and no information is rolled back.
+-/
 @[always_inline, inline]
 protected def tryCatch {δ} [Backtrackable δ σ] {α} (x : EStateM ε σ α) (handle : ε → EStateM ε σ α) : EStateM ε σ α := fun s =>
   let d := Backtrackable.save s
@@ -3701,7 +3823,14 @@ protected def tryCatch {δ} [Backtrackable δ σ] {α} (x : EStateM ε σ α) (h
   | Result.error e s => handle e (Backtrackable.restore s d)
   | ok               => ok
 
-/-- Implementation of `orElse` for `EStateM` where the state is `Backtrackable`. -/
+/--
+Failure handling that does not depend on specific exception values.
+
+The `Backtrackable δ σ` instance is used to save a snapshot of part of the state prior to running
+`x₁`. If an exception is caught, the state is updated with the saved snapshot, rolling back part of
+the state. If no instance of `Backtrackable` is provided, a fallback instance in which `δ` is `Unit`
+is used, and no information is rolled back.
+-/
 @[always_inline, inline]
 protected def orElse {δ} [Backtrackable δ σ] (x₁ : EStateM ε σ α) (x₂ : Unit → EStateM ε σ α) : EStateM ε σ α := fun s =>
   let d := Backtrackable.save s;
@@ -3709,28 +3838,37 @@ protected def orElse {δ} [Backtrackable δ σ] (x₁ : EStateM ε σ α) (x₂
   | Result.error _ s => x₂ () (Backtrackable.restore s d)
   | ok               => ok
 
-/-- Map the exception type of a `EStateM ε σ α` by a function `f : ε → ε'`. -/
+/--
+Transforms exceptions with a function, doing nothing on successful results.
+-/
 @[always_inline, inline]
 def adaptExcept {ε' : Type u} (f : ε → ε') (x : EStateM ε σ α) : EStateM ε' σ α := fun s =>
   match x s with
   | Result.error e s => Result.error (f e) s
   | Result.ok a s    => Result.ok a s
 
-/-- The `bind` operation of the `EStateM` monad. -/
+/--
+Sequences two `EStateM ε σ` actions, passing the returned value from the first into the second.
+-/
 @[always_inline, inline]
 protected def bind (x : EStateM ε σ α) (f : α → EStateM ε σ β) : EStateM ε σ β := fun s =>
   match x s with
   | Result.ok a s    => f a s
   | Result.error e s => Result.error e s
 
-/-- The `map` operation of the `EStateM` monad. -/
+/--
+Transforms the value returned from an `EStateM ε σ` action using a function.
+-/
 @[always_inline, inline]
 protected def map (f : α → β) (x : EStateM ε σ α) : EStateM ε σ β := fun s =>
   match x s with
   | Result.ok a s    => Result.ok (f a) s
   | Result.error e s => Result.error e s
 
-/-- The `seqRight` operation of the `EStateM` monad. -/
+/--
+Sequences two `EStateM ε σ` actions, running `x` before `y`. The first action's return value is
+ignored.
+-/
 @[always_inline, inline]
 protected def seqRight (x : EStateM ε σ α) (y : Unit → EStateM ε σ β) : EStateM ε σ β := fun s =>
   match x s with
@@ -3756,13 +3894,16 @@ instance {δ} [Backtrackable δ σ] : MonadExceptOf ε (EStateM ε σ) where
   throw    := EStateM.throw
   tryCatch := EStateM.tryCatch
 
-/-- Execute an `EStateM` on initial state `s` to get a `Result`. -/
+/--
+Executes an `EStateM` action with the initial state `s`. The returned value includes the final state
+and indicates whether an exception was thrown or a value was returned.
+-/
 @[always_inline, inline]
 def run (x : EStateM ε σ α) (s : σ) : Result ε σ α := x s
 
 /--
-Execute an `EStateM` on initial state `s` for the returned value `α`.
-If the monadic action throws an exception, returns `none` instead.
+Executes an `EStateM` with the initial state `s` for the returned value `α`, discarding the final
+state. Returns `none` if an unhandled exception was thrown.
 -/
 @[always_inline, inline]
 def run' (x : EStateM ε σ α) (s : σ) : Option α :=
@@ -3777,10 +3918,11 @@ def run' (x : EStateM ε σ α) (s : σ) : Option α :=
 @[inline] def dummyRestore : σ → PUnit → σ := fun s _ => s
 
 /--
-Dummy default instance. This makes every `σ` trivially "backtrackable"
-by doing nothing on backtrack. Because this is the first declared instance
-of `Backtrackable _ σ`, it will be picked only if there are no other
-`Backtrackable _ σ` instances registered.
+A fallback `Backtrackable` instance that saves no information from a state. This allows every type
+to be used as a state in `EStateM`, with no rollback.
+
+Because this is the first declared instance of `Backtrackable _ σ`, it will be picked only if there
+are no other `Backtrackable _ σ` instances registered.
 -/
 instance nonBacktrackable : Backtrackable PUnit σ where
   save    := dummySave
diff --git a/src/Lean/Meta/Coe.lean b/src/Lean/Meta/Coe.lean
index 5527ff1cf2..ed94cf3e4c 100644
--- a/src/Lean/Meta/Coe.lean
+++ b/src/Lean/Meta/Coe.lean
@@ -34,7 +34,7 @@ partial def expandCoe (e : Expr) : MetaM Expr :=
 
 register_builtin_option autoLift : Bool := {
   defValue := true
-  descr    := "insert monadic lifts (i.e., `liftM` and coercions) when needed"
+  descr    := "Insert monadic lifts (i.e., `liftM` and coercions) when needed."
 }
 
 /-- Coerces `expr` to `expectedType` using `CoeT`. -/
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 0c42b6fe0e..d99a5118ea 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -1009,6 +1009,12 @@ def macroArg       := termParser maxPrec
 def macroDollarArg := leading_parser "$" >> termParser 10
 def macroLastArg   := macroDollarArg <|> macroArg
 
+/--
+A state monad that uses an actual mutable reference cell (i.e. an `ST.Ref`).
+
+This is syntax, rather than a function, to make it easier to use. Its elaborator synthesizes an
+appropriate parameter for the underlying monad's `ST` effects, then passes it to `StateRefT'`.
+-/
 -- Macro for avoiding exponentially big terms when using `STWorld`
 @[builtin_term_parser] def stateRefT := leading_parser
   "StateRefT " >> macroArg >> ppSpace >> macroLastArg