diff --git a/src/Std/Do/PostCond.lean b/src/Std/Do/PostCond.lean
index 01f165c5afdf..a318b58a4d70 100644
--- a/src/Std/Do/PostCond.lean
+++ b/src/Std/Do/PostCond.lean
@@ -10,6 +10,8 @@ public import Std.Do.SPred
 
 @[expose] public section
 
+set_option linter.missingDocs true
+
 /-!
 # Pre and postconditions
 
@@ -44,51 +46,86 @@ namespace Std.Do
 
 universe u
 
+/--
+The “shape” of the postconditions that are used to reason about a monad.
+
+A postcondition shape is an abstraction of many possible monadic effects, based on the structure of pure functions that can simulate them. The postcondition shape of a monad is given by its `WP` instance. This shape is used to determine both its `Assertion`s and its `PostCond`s.
+-/
 inductive PostShape : Type (u+1) where
+  /-- The assertions and postconditions in this monad use neither state nor exceptions. -/
   | pure : PostShape
+  /--
+  The assertions in this monad may mention the current value of a state of type `σ`, and
+  postconditions may mention the state's final value.
+  -/
   | arg : (σ : Type u) → PostShape → PostShape
+  /--
+  The postconditions in this monad include assertions about exceptional values of type `ε` that
+  result from premature termination.
+  -/
   | except : (ε : Type u) → PostShape → PostShape
 
 variable {ps : PostShape.{u}} {α σ ε : Type u}
 
+/--
+Extracts the list of state types under `PostShape.arg` constructors, discarding exception types.
+
+The state types determine the shape of assertions in the monad.
+-/
 abbrev PostShape.args : PostShape.{u} → List (Type u)
   | .pure => []
   | .arg σ s => σ :: PostShape.args s
   | .except _ s => PostShape.args s
 
 /--
-  An assertion on the `.arg`s in the given predicate shape.
-  ```
-  example : Assertion (.arg ρ .pure) = (ρ → ULift Prop) := rfl
-  example : Assertion (.except ε .pure) = ULift Prop := rfl
-  example : Assertion (.arg σ (.except ε .pure)) = (σ → ULift Prop) := rfl
-  example : Assertion (.except ε (.arg σ .pure)) = (σ → ULift Prop) := rfl
-  ```
-  This is an abbreviation for `SPred` under the hood, so all theorems about `SPred` apply.
+An assertion about the state fields for a monad whose postcondition shape is `ps`.
+
+Concretely, this is an abbreviation for `SPred` applied to the `.arg`s in the given predicate shape, so all theorems about `SPred` apply.
+
+Examples:
+```lean example
+example : Assertion (.arg ρ .pure) = (ρ → ULift Prop) := rfl
+example : Assertion (.except ε .pure) = ULift Prop := rfl
+example : Assertion (.arg σ (.except ε .pure)) = (σ → ULift Prop) := rfl
+example : Assertion (.except ε (.arg σ .pure)) = (σ → ULift Prop) := rfl
+```
 -/
 abbrev Assertion (ps : PostShape.{u}) : Type u :=
   SPred (PostShape.args ps)
 
 /--
-  Encodes one continuation barrel for each `PostShape.except` in the given predicate shape.
-  ```
-  example : ExceptConds (.pure) = Unit := rfl
-  example : ExceptConds (.except ε .pure) = ((ε → ULift Prop) × Unit) := rfl
-  example : ExceptConds (.arg σ (.except ε .pure)) = ((ε → ULift Prop) × Unit) := rfl
-  example : ExceptConds (.except ε (.arg σ .pure)) = ((ε → σ → ULift Prop) × Unit) := rfl
-  ```
+An assertion about each potential exception that's declared in a postcondition shape.
+
+Examples:
+```lean example
+example : ExceptConds (.pure) = Unit := rfl
+example : ExceptConds (.except ε .pure) = ((ε → ULift Prop) × Unit) := rfl
+example : ExceptConds (.arg σ (.except ε .pure)) = ((ε → ULift Prop) × Unit) := rfl
+example : ExceptConds (.except ε (.arg σ .pure)) = ((ε → σ → ULift Prop) × Unit) := rfl
+```
 -/
 def ExceptConds : PostShape.{u} → Type u
   | .pure => PUnit
   | .arg _ ps => ExceptConds ps
   | .except ε ps => (ε → Assertion ps) × ExceptConds ps
 
+/--
+Lifts a proposition `p` to a set of assertions about the possible exceptions in `ps`. Each
+exception's postcondition holds when `p` is true.
+-/
 def ExceptConds.const {ps : PostShape.{u}} (p : Prop) : ExceptConds ps := match ps with
   | .pure => ⟨⟩
   | .arg _ ps => @ExceptConds.const ps p
   | .except _ ps => (fun _ε => spred(⌜p⌝), @ExceptConds.const ps p)
 
+/--
+An assertion about the possible exceptions in `ps` that always holds.
+-/
 def ExceptConds.true : ExceptConds ps := ExceptConds.const True
+
+/--
+An assertion about the possible exceptions in `ps` that never holds.
+-/
 def ExceptConds.false : ExceptConds ps := ExceptConds.const False
 
 @[simp, grind =]
@@ -118,12 +155,20 @@ theorem ExceptConds.snd_false {ps : PostShape.{u}} :
 instance : Inhabited (ExceptConds ps) where
   default := ExceptConds.true
 
+/--
+Entailment of exception assertions is defined as pointwise entailment of the assertions for each
+potential exception.
+
+While implication of exception conditions (`ExceptConds.imp`) is itself an exception condition,
+entailment is an ordinary proposition.
+-/
 def ExceptConds.entails {ps : PostShape.{u}} (x y : ExceptConds ps) : Prop :=
   match ps with
   | .pure => True
   | .arg _ ps => @entails ps x y
   | .except _ ps => (∀ e, x.1 e ⊢ₛ y.1 e) ∧ @entails ps x.2 y.2
 
+@[inherit_doc ExceptConds.entails]
 scoped infixr:25 " ⊢ₑ " => ExceptConds.entails
 
 @[refl, simp]
@@ -146,12 +191,17 @@ theorem ExceptConds.entails_false {x : ExceptConds ps} : ExceptConds.false ⊢
 theorem ExceptConds.entails_true {x : ExceptConds ps} : x ⊢ₑ ExceptConds.true := by
   induction ps <;> simp_all [true, const, entails]
 
+/--
+Conjunction of exception assertions is defined as pointwise conjunction of the assertions for each
+potential exception.
+-/
 def ExceptConds.and {ps : PostShape.{u}} (x : ExceptConds ps) (y : ExceptConds ps) : ExceptConds ps :=
   match ps with
   | .pure => ⟨⟩
   | .arg _ ps => @ExceptConds.and ps x y
   | .except _ _ => (fun e => SPred.and (x.1 e) (y.1 e), ExceptConds.and x.2 y.2)
 
+@[inherit_doc ExceptConds.and]
 infixr:35 " ∧ₑ " => ExceptConds.and
 
 @[simp]
@@ -207,12 +257,20 @@ theorem ExceptConds.and_eq_left {ps : PostShape} {p q : ExceptConds ps} (h : p 
     · ext a; exact (SPred.and_eq_left.mp (h.1 a)).to_eq
     · exact ih h.2
 
+/--
+Implication of exception assertions is defined as pointwise implication of the assertion for each
+exception.
+
+Unlike entailment (`ExceptConds.entails`), which is an ordinary proposition of type `Prop`,
+implication of exception assertions is itself an exception assertion.
+-/
 def ExceptConds.imp {ps : PostShape.{u}} (x : ExceptConds ps) (y : ExceptConds ps) : ExceptConds ps :=
   match ps with
   | .pure => ⟨⟩
   | .arg _ ps => @ExceptConds.imp ps x y
   | .except _ _ => (fun e => SPred.imp (x.1 e) (y.1 e), ExceptConds.imp x.2 y.2)
 
+@[inherit_doc ExceptConds.imp]
 infixr:25 " →ₑ " => ExceptConds.imp
 
 @[simp]
@@ -304,10 +362,21 @@ scoped macro:max ppAllowUngrouped "⇓?" xs:term:max+ " => " e:term : term =>
 instance : Inhabited (PostCond α ps) where
   default := PostCond.noThrow fun _ => default
 
+/--
+Entailment of postconditions.
+
+This consists of:
+ * Entailment of the assertion about the return value, for all possible return values.
+ * Entailment of the exception conditions.
+
+While implication of postconditions (`PostCond.imp`) results in a new postcondition, entailment is
+an ordinary proposition.
+-/
 @[simp]
 def PostCond.entails (p q : PostCond α ps) : Prop :=
   (∀ a, SPred.entails (p.1 a) (q.1 a)) ∧ ExceptConds.entails p.2 q.2
 
+@[inherit_doc PostCond.entails]
 scoped infixr:25 " ⊢ₚ " => PostCond.entails
 
 @[refl, simp]
@@ -325,14 +394,31 @@ theorem PostCond.entails_noThrow (p : α → Assertion ps) (q : PostCond α ps)
 theorem PostCond.entails_mayThrow (p : PostCond α ps) (q : α → Assertion ps) : p ⊢ₚ PostCond.mayThrow q ↔ ∀ a, p.1 a ⊢ₛ q a := by
   simp only [entails, ExceptConds.entails_true, and_true]
 
+/--
+Conjunction of postconditions.
+
+This is defined pointwise, as the conjunction of the assertions about the return value and the
+conjunctions of the assertions about each potential exception.
+-/
 abbrev PostCond.and (p : PostCond α ps) (q : PostCond α ps) : PostCond α ps :=
   (fun a => SPred.and (p.1 a) (q.1 a), ExceptConds.and p.2 q.2)
 
+@[inherit_doc PostCond.and]
 scoped infixr:35 " ∧ₚ " => PostCond.and
 
+/--
+Implication of postconditions.
+
+This is defined pointwise, as the implication of the assertions about the return value and the
+implications of each of the assertions about each potential exception.
+
+While entailment of postconditions (`PostCond.entails`) is an ordinary proposition, implication of
+postconditions is itself a postcondition.
+-/
 abbrev PostCond.imp (p : PostCond α ps) (q : PostCond α ps) : PostCond α ps :=
   (fun a => SPred.imp (p.1 a) (q.1 a), ExceptConds.imp p.2 q.2)
 
+@[inherit_doc PostCond.imp]
 scoped infixr:25 " →ₚ " => PostCond.imp
 
 theorem PostCond.and_imp : P' ∧ₚ (P' →ₚ Q') ⊢ₚ P' ∧ₚ Q' := by
diff --git a/src/Std/Do/PredTrans.lean b/src/Std/Do/PredTrans.lean
index 1fa5d70974b3..21c8f2d2c6a8 100644
--- a/src/Std/Do/PredTrans.lean
+++ b/src/Std/Do/PredTrans.lean
@@ -11,6 +11,8 @@ public import Std.Do.PostCond
 
 @[expose] public section
 
+set_option linter.missingDocs true
+
 /-!
 # Predicate transformers for arbitrary postcondition shapes
 
@@ -54,9 +56,9 @@ def PredTrans.Conjunctive.mono (t : PostCond α ps → Assertion ps) (h : PredTr
   exact SPred.and_elim_r
 
 /--
-  The type of predicate transformers for a given `ps : PostShape` and return type `α : Type`.
-  A predicate transformer `x : PredTrans ps α` is a function that takes a postcondition
-  `Q : PostCond α ps` and returns a precondition `x.apply Q : Assertion ps`.
+The type of predicate transformers for a given `ps : PostShape` and return type `α : Type`. A
+predicate transformer `x : PredTrans ps α` is a function that takes a postcondition `Q : PostCond α
+ps` and returns a precondition `x.apply Q : Assertion ps`.
  -/
 @[ext]
 structure PredTrans (ps : PostShape) (α : Type u) : Type u where
@@ -72,16 +74,23 @@ theorem mono (t : PredTrans ps α) : Monotonic t.apply :=
   Conjunctive.mono t.apply t.conjunctive
 
 /--
-  Given a fixed postcondition, the *stronger* predicate transformer will yield a
-  *weaker* precondition.
+Given a fixed postcondition, the *stronger* predicate transformer will yield a *weaker*
+precondition.
 -/
 def le (x y : PredTrans ps α) : Prop :=
-  ∀ Q, y.apply Q ⊢ₛ x.apply Q -- the weaker the precondition, the smaller the PredTrans
+  ∀ Q, y.apply Q ⊢ₛ x.apply Q
 instance : LE (PredTrans ps α) := ⟨le⟩
 
+/--
+The identity predicate transformer that transforms the postcondition's assertion about the return
+value into an assertion about `a`.
+-/
 def pure (a : α) : PredTrans ps α :=
   { apply := fun Q => Q.1 a, conjunctive := by intro _ _; simp }
 
+/--
+Sequences two predicate transformers by composing them.
+-/
 def bind (x : PredTrans ps α) (f : α → PredTrans ps β) : PredTrans ps β :=
   { apply := fun Q => x.apply (fun a => (f a).apply Q, Q.2),
     conjunctive := by
@@ -135,7 +144,14 @@ instance instLawfulMonad : LawfulMonad (PredTrans ps) :=
     (pure_bind := by simp +unfoldPartialApp [Bind.bind, bind, Pure.pure, pure])
     (bind_assoc := by simp +unfoldPartialApp [Bind.bind, bind])
 
--- The interpretation of `StateT σ (PredTrans ps) α` into `PredTrans (.arg σ ps) α`.
+/--
+Adds the ability to make assertions about a state of type `σ` to a predicate transformer with
+postcondition shape `ps`, resulting in postcondition shape `.arg σ ps`. This is done by
+interpreting `StateT σ (PredTrans ps) α` into `PredTrans (.arg σ ps) α`.
+
+This can be used to for all kinds of state-like effects, including reader effects or append-only
+states, by interpreting them as states.
+-/
 -- Think: modifyGetM
 def pushArg {σ : Type u} (x : StateT σ (PredTrans ps) α) : PredTrans (.arg σ ps) α where
   apply := fun Q s => (x s).apply (fun (a, s) => Q.1 a s, Q.2)
@@ -146,7 +162,14 @@ def pushArg {σ : Type u} (x : StateT σ (PredTrans ps) α) : PredTrans (.arg σ
     dsimp only [SPred.and_cons, ExceptConds.and]
     rw [← ((x s).conjunctive _ _).to_eq]
 
--- The interpretation of `ExceptT ε (PredTrans ps) α` into `PredTrans (.except ε ps) α`
+/--
+Adds the ability to make assertions about exceptions of type `ε` to a predicate transformer with
+postcondition shape `ps`, resulting in postcondition shape `.except ε ps`. This is done by
+interpreting `ExceptT ε (PredTrans ps) α` into `PredTrans (.except ε ps) α`.
+
+This can be used for all kinds of exception-like effects, such as early termination, by interpreting
+them as exceptions.
+-/
 def pushExcept {ps : PostShape} {α ε} (x : ExceptT ε (PredTrans ps) α) : PredTrans (.except ε ps) α where
   apply Q := x.apply (fun | .ok a => Q.1 a | .error e => Q.2.1 e, Q.2.2)
   conjunctive := by
@@ -158,6 +181,12 @@ def pushExcept {ps : PostShape} {α ε} (x : ExceptT ε (PredTrans ps) α) : Pre
     ext x
     cases x <;> simp
 
+/--
+Adds the ability to make assertions about early termination to a predicate transformer with
+postcondition shape `ps`, resulting in postcondition shape `.except PUnit ps`. This is done by
+interpreting `OptionT (PredTrans ps) α` into `PredTrans (.except PUnit ps) α`, which models the type
+`Option` as being equivalent to `Except PUnit`.
+-/
 def pushOption {ps : PostShape} {α} (x : OptionT (PredTrans ps) α) : PredTrans (.except PUnit ps) α where
   apply Q := x.apply (fun | .some a => Q.1 a | .none => Q.2.1 ⟨⟩, Q.2.2)
   conjunctive := by
@@ -170,19 +199,19 @@ def pushOption {ps : PostShape} {α} (x : OptionT (PredTrans ps) α) : PredTrans
     cases x <;> simp
 
 @[simp]
-def pushArg_apply {ps} {α σ : Type u} {Q : PostCond α (.arg σ ps)} (f : σ → PredTrans ps (α × σ)) :
+theorem pushArg_apply {ps} {α σ : Type u} {Q : PostCond α (.arg σ ps)} (f : σ → PredTrans ps (α × σ)) :
   (pushArg f).apply Q = fun s => (f s).apply (fun ⟨a, s⟩ => Q.1 a s, Q.2) := rfl
 
 @[simp]
-def pushExcept_apply {ps} {α ε : Type u} {Q : PostCond α (.except ε ps)} (x : PredTrans ps (Except ε α)) :
+theorem pushExcept_apply {ps} {α ε : Type u} {Q : PostCond α (.except ε ps)} (x : PredTrans ps (Except ε α)) :
   (pushExcept x).apply Q = x.apply (fun | .ok a => Q.1 a | .error e => Q.2.1 e, Q.2.2) := rfl
 
 @[simp]
-def pushOption_apply {ps} {α : Type u} {Q : PostCond α (.except PUnit ps)} (x : PredTrans ps (Option α)) :
+theorem pushOption_apply {ps} {α : Type u} {Q : PostCond α (.except PUnit ps)} (x : PredTrans ps (Option α)) :
   (pushOption x).apply Q = x.apply (fun | .some a => Q.1 a | .none => Q.2.1 ⟨⟩, Q.2.2) := rfl
 
-def dite_apply {ps} {Q : PostCond α ps} (c : Prop) [Decidable c] (t : c → PredTrans ps α) (e : ¬ c → PredTrans ps α) :
+theorem dite_apply {ps} {Q : PostCond α ps} (c : Prop) [Decidable c] (t : c → PredTrans ps α) (e : ¬ c → PredTrans ps α) :
   (if h : c then t h else e h).apply Q = if h : c then (t h).apply Q else (e h).apply Q := by split <;> rfl
 
-def ite_apply {ps} {Q : PostCond α ps} (c : Prop) [Decidable c] (t : PredTrans ps α) (e : PredTrans ps α) :
+theorem ite_apply {ps} {Q : PostCond α ps} (c : Prop) [Decidable c] (t : PredTrans ps α) (e : PredTrans ps α) :
   (if c then t else e).apply Q = if c then t.apply Q else e.apply Q := by split <;> rfl
diff --git a/src/Std/Do/SPred.lean b/src/Std/Do/SPred.lean
index 383409a965e9..7f8612518db5 100644
--- a/src/Std/Do/SPred.lean
+++ b/src/Std/Do/SPred.lean
@@ -11,3 +11,5 @@ public import Std.Do.SPred.SPred
 public import Std.Do.SPred.Notation
 public import Std.Do.SPred.Laws
 public import Std.Do.SPred.DerivedLaws
+
+set_option linter.missingDocs true
diff --git a/src/Std/Do/SPred/DerivedLaws.lean b/src/Std/Do/SPred/DerivedLaws.lean
index 0eb5369ebe83..80876932559c 100644
--- a/src/Std/Do/SPred/DerivedLaws.lean
+++ b/src/Std/Do/SPred/DerivedLaws.lean
@@ -11,6 +11,8 @@ public import Std.Do.SPred.Laws
 
 @[expose] public section
 
+set_option linter.missingDocs true
+
 /-!
 # Derived laws of `SPred`
 
@@ -180,13 +182,25 @@ namespace Tactic
 /-- Tautology in `SPred` as a quotable definition. -/
 abbrev tautological (Q : SPred σs) : Prop := ⊢ₛ Q
 
+/--
+A mapping from propositions to `SPred` tautologies that are known to be logically equivalent.
+This is used to rewrite proof goals into a form that is suitable for use with `mvcgen`.
+-/
 class PropAsSPredTautology (φ : Prop) {σs : outParam (List (Type u))} (P : outParam (SPred σs)) : Prop where
+  /-- A proof that `φ` and `P` are logically equivalent. -/
   iff : φ ↔ ⊢ₛ P
 instance {φ : SPred []} : PropAsSPredTautology φ.down φ where iff := true_imp_iff.symm
 instance : PropAsSPredTautology (P ⊢ₛ Q) spred(P → Q) where iff := iff_of_eq (entails_true_intro P Q).symm
 instance : PropAsSPredTautology (⊢ₛ P) P where iff := Iff.rfl
 
-class IsPure (P : SPred σs) (φ : outParam Prop) where to_pure : P ⊣⊢ₛ ⌜φ⌝
+/--
+A mapping from `SPred` to pure propositions that are known to be equivalent.
+-/
+class IsPure (P : SPred σs) (φ : outParam Prop) where
+  /--
+  A proof that `P` and `φ` are equivalent.
+  -/
+  to_pure : P ⊣⊢ₛ ⌜φ⌝
 instance (σs) : IsPure (σs:=σs) ⌜φ⌝ φ where to_pure := .rfl
 instance (σs) : IsPure (σs:=σs) spred(⌜φ⌝ → ⌜ψ⌝) (φ → ψ) where to_pure := pure_imp
 instance (σs) : IsPure (σs:=σs) spred(⌜φ⌝ ∧ ⌜ψ⌝) (φ ∧ ψ) where to_pure := pure_and
@@ -198,7 +212,14 @@ instance (σs) (P : SPred σs) [inst : IsPure P φ] : IsPure (σs:=σ::σs) (fun
 instance (φ : Prop) : IsPure (σs:=[]) ⌜φ⌝ φ where to_pure := Iff.rfl
 instance (P : SPred []) : IsPure (σs:=[]) P P.down where to_pure := Iff.rfl
 
+/--
+A decomposition of a stateful predicate into the conjunction of two other stateful predicates.
+
+Decomposing assertions in postconditions into conjunctions of simpler predicates increases the
+chance that automation will be able to prove the entailment of the postcondition and the next precondition.
+-/
 class IsAnd (P : SPred σs) (Q₁ Q₂ : outParam (SPred σs)) where
+  /-- A proof the the decomposition is logically equivalent to the original predicate. -/
   to_and : P ⊣⊢ₛ Q₁ ∧ Q₂
 instance (σs) (Q₁ Q₂ : SPred σs) : IsAnd (σs:=σs) spred(Q₁ ∧ Q₂) Q₁ Q₂ where to_and := .rfl
 instance (σs) : IsAnd (σs:=σs) ⌜p ∧ q⌝ ⌜p⌝ ⌜q⌝ where to_and := pure_and.symm
@@ -256,13 +277,25 @@ theorem Specialize.pure_start {φ : Prop} {H P T : SPred σs} [PropAsSPredTautol
 theorem Specialize.pure_taut {σs} {φ} {P : SPred σs} [IsPure P φ] (h : φ) : ⊢ₛ P := (pure_intro h).trans IsPure.to_pure.mpr
 theorem Specialize.focus {P P' Q R : SPred σs} (hfocus : P ⊣⊢ₛ P' ∧ Q) (hnew : P' ∧ Q ⊢ₛ R) : P ⊢ₛ R := hfocus.mp.trans hnew
 
+/--
+Expresses that the conjunction of `P` and `Q` is equivalent to `spred(P ∧ Q)`, but potentially
+simpler.
+-/
 class SimpAnd (P Q : SPred σs) (PQ : outParam (SPred σs)) : Prop where
+  /-- A proof that `spred(P ∧ Q)` is logically equivalent to `PQ`.-/
   simp_and : P ∧ Q ⊣⊢ₛ PQ
 instance (σs) (P Q : SPred σs) : SimpAnd P Q (spred(P ∧ Q)) where simp_and := .rfl
 instance (σs) (P : SPred σs) : SimpAnd P ⌜True⌝ P where simp_and := and_true
 instance (σs) (P : SPred σs) : SimpAnd ⌜True⌝ P P where simp_and := true_and
 
+/--
+Provides a decomposition of a stateful predicate (`P`) into stateful and pure components (`P'` and
+`φ`, respectively).
+-/
 class HasFrame (P : SPred σs) (P' : outParam (SPred σs)) (φ : outParam Prop) : Prop where
+  /--
+  A proof that the original stateful predicate is equivalent to the decomposed form.
+  -/
   reassoc : P ⊣⊢ₛ P' ∧ ⌜φ⌝
 instance (σs) (P P' Q QP : SPred σs) [HasFrame P Q φ] [SimpAnd Q P' QP]: HasFrame (σs:=σs) spred(P ∧ P') QP φ where reassoc := ((and_congr_l HasFrame.reassoc).trans and_right_comm).trans (and_congr_l SimpAnd.simp_and)
 instance (σs) (P P' Q' PQ : SPred σs) [HasFrame P' Q' φ] [SimpAnd P Q' PQ]: HasFrame (σs:=σs) spred(P ∧ P') PQ φ where reassoc := ((and_congr_r HasFrame.reassoc).trans and_assoc.symm).trans (and_congr_l SimpAnd.simp_and)
diff --git a/src/Std/Do/SPred/Laws.lean b/src/Std/Do/SPred/Laws.lean
index 8cca033a8dc2..4ce244e7b83e 100644
--- a/src/Std/Do/SPred/Laws.lean
+++ b/src/Std/Do/SPred/Laws.lean
@@ -10,6 +10,8 @@ public import Std.Do.SPred.Notation
 
 @[expose] public section
 
+set_option linter.missingDocs true
+
 namespace Std.Do.SPred
 
 /-!
diff --git a/src/Std/Do/SPred/Notation.lean b/src/Std/Do/SPred/Notation.lean
index 17bbd098e687..91b0a89b05b6 100644
--- a/src/Std/Do/SPred/Notation.lean
+++ b/src/Std/Do/SPred/Notation.lean
@@ -11,6 +11,8 @@ public meta import Std.Do.SPred.Notation.Basic
 
 public section
 
+set_option linter.missingDocs true
+
 namespace Std.Do
 
 open Lean Macro Parser PrettyPrinter
@@ -53,12 +55,18 @@ macro_rules
 
 namespace SPred.Notation
 
+/--
+Unexpander that reconstructs `⌜...⌝` syntax from applications of `SPred.pure`.
+-/
 @[app_unexpander SPred.pure]
 meta def unexpandPure : Unexpander
   | `($_ $t $ts*) => do
     if ts.isEmpty then ``(⌜$t⌝) else ``(⌜$t⌝ $ts*)
   | _ => throw ()
 
+/--
+Unexpander that reconstructs `... ⊢ₛ ...⌝` syntax from applications of `SPred.entails`.
+-/
 @[app_unexpander SPred.entails]
 meta def unexpandEntails : Unexpander
   | `($_ $P $Q)  => do
@@ -68,6 +76,9 @@ meta def unexpandEntails : Unexpander
     | _ => ``($P ⊢ₛ $Q)
   | _ => throw ()
 
+/--
+Unexpander that reconstructs `... ⊣⊢ₛ ...⌝` syntax from applications of `SPred.entails`.
+-/
 @[app_unexpander SPred.bientails]
 meta def unexpandBientails : Unexpander
   | `($_ $P $Q)  => do
@@ -75,6 +86,10 @@ meta def unexpandBientails : Unexpander
     ``($P ⊣⊢ₛ $Q)
   | _ => throw ()
 
+/--
+Unexpander that reconstructs `spred(... ∧ ...)⌝` syntax from applications of `SPred.and`, lifting
+nested applications of `spred(...)` from the arguments.
+-/
 @[app_unexpander SPred.and]
 meta def unexpandAnd : Unexpander
   | `($_ $P $Q) => do
@@ -82,6 +97,10 @@ meta def unexpandAnd : Unexpander
     ``(spred($P ∧ $Q))
   | _ => throw ()
 
+/--
+Unexpander that reconstructs `spred(... ∨ ...)⌝` syntax from applications of `SPred.or`, lifting
+nested applications of `spred(...)` from the arguments.
+-/
 @[app_unexpander SPred.or]
 meta def unexpandOr : Unexpander
   | `($_ $P $Q) => do
@@ -89,6 +108,10 @@ meta def unexpandOr : Unexpander
     ``(spred($P ∨ $Q))
   | _ => throw ()
 
+/--
+Unexpander that reconstructs `spred(¬ ...)⌝` syntax from applications of `SPred.not`, lifting
+nested applications of `spred(...)` from the argument.
+-/
 @[app_unexpander SPred.not]
 meta def unexpandNot : Unexpander
   | `($_ $P) => do
@@ -96,6 +119,10 @@ meta def unexpandNot : Unexpander
     ``(spred(¬ $P))
   | _ => throw ()
 
+/--
+Unexpander that reconstructs `spred(... → ...)⌝` syntax from applications of `SPred.imp`, lifting
+nested applications of `spred(...)` from the arguments.
+-/
 @[app_unexpander SPred.imp]
 meta def unexpandImp : Unexpander
   | `($_ $P $Q) => do
@@ -103,6 +130,10 @@ meta def unexpandImp : Unexpander
     ``(spred($P → $Q))
   | _ => throw ()
 
+/--
+Unexpander that reconstructs `spred(∀ ..., ...)⌝` syntax from applications of `SPred.forall`, lifting
+nested applications of `spred(...)` from the body.
+-/
 @[app_unexpander SPred.forall]
 meta def unexpandForall : Unexpander
   | `($_ fun $x:ident => ∀ $y:ident $[$z:ident]*, $Ψ) => do
@@ -113,6 +144,10 @@ meta def unexpandForall : Unexpander
     ``(spred(∀ $x:ident, $Ψ))
   | _ => throw ()
 
+/--
+Unexpander that reconstructs `spred(∃ ..., ...)⌝` syntax from applications of `SPred.exists`, lifting
+nested applications of `spred(...)` from the body.
+-/
 @[app_unexpander SPred.exists]
 meta def unexpandExists : Unexpander
   | `($_ fun $x:ident => ∃ $y:ident $[$z:ident]*, $Ψ) => do
@@ -123,6 +158,10 @@ meta def unexpandExists : Unexpander
     ``(spred(∃ $x:ident, $Ψ))
   | _ => throw ()
 
+/--
+Unexpander that reconstructs `spred(... ↔ ...)⌝` syntax from applications of `SPred.iff`, lifting
+nested applications of `spred(...)` from the arguments.
+-/
 @[app_unexpander SPred.iff]
 meta def unexpandIff : Unexpander
   | `($_ $P $Q) => do
diff --git a/src/Std/Do/SPred/Notation/Basic.lean b/src/Std/Do/SPred/Notation/Basic.lean
index 572ba8a912ca..065c7c85e2d8 100644
--- a/src/Std/Do/SPred/Notation/Basic.lean
+++ b/src/Std/Do/SPred/Notation/Basic.lean
@@ -11,6 +11,8 @@ import Init.NotationExtra
 
 public section
 
+set_option linter.missingDocs true
+
 namespace Std.Do
 
 open Lean Macro Parser PrettyPrinter
@@ -18,7 +20,17 @@ open Lean Macro Parser PrettyPrinter
 -- define `spred` embedding in `term`.
 -- An explicit `spred` marker avoids exponential blowup in terms
 -- that do not opt into the extended syntax.
+/--
+An embedding of the special syntax for `SPred` into ordinary terms that provides alternative
+interpretations of logical connectives and quantifiers.
+
+Within `spred(...)`, `term(...)` escapes to the ordinary Lean interpretation of this syntax.
+-/
 scoped syntax:max "spred(" term ")" : term
+/--
+Escapes from a surrounding `spred(...)` term, returning to the usual interpretations of quantifiers
+and connectives.
+-/
 scoped syntax:max "term(" term ")" : term
 
 -- allow fallback to `term`
@@ -26,14 +38,14 @@ macro_rules
   | `(spred(term($t))) => pure t
   | `(spred($t))       => pure t
 
--- push `spred` inside some `term` constructs
+-- pushes `spred` inside some `term` constructs
 macro_rules
   | `(spred(($P)))                  => ``((spred($P)))
   | `(spred(fun $xs* => $b))        => ``(fun $xs* => spred($b))
   | `(spred(if $c then $t else $e)) => ``(if $c then spred($t) else spred($e))
   | `(spred(($P : $t)))             => ``((spred($P) : $t))
 
-/-- Remove an `spred` layer from a `term` syntax object. -/
+/-- Removes an `spred` layer from a `term` syntax object. -/
 -- inverts the rules above.
 partial def SPred.Notation.unpack [Monad m] [MonadRef m] [MonadQuotation m] : Term → m Term
   | `(spred($P))             => do `($P)
diff --git a/src/Std/Do/SPred/SPred.lean b/src/Std/Do/SPred/SPred.lean
index 72eef379bb73..2b11430d1e8a 100644
--- a/src/Std/Do/SPred/SPred.lean
+++ b/src/Std/Do/SPred/SPred.lean
@@ -11,6 +11,8 @@ public import Std.Do.SPred.SVal
 
 @[expose] public section
 
+set_option linter.missingDocs true
+
 /-!
 # State-indexed predicates
 
@@ -21,10 +23,12 @@ This type forms the basis for the notion of assertion in `Std.Do`; see `Std.Do.A
 namespace Std.Do
 
 /--
-  A predicate indexed by a list of states.
-  ```
-  example : SPred [Nat, Bool] = (Nat → Bool → ULift Prop) := rfl
-  ```
+A predicate over states, where each state is defined by a list of component state types.
+
+Example:
+```lean example
+SPred [Nat, Bool] = (Nat → Bool → ULift Prop)
+```
 -/
 abbrev SPred (σs : List (Type u)) : Type u := SVal σs (ULift Prop)
 
@@ -42,7 +46,7 @@ theorem ext_cons {P Q : SPred (σ::σs)} : (∀ s, P s = Q s) → P = Q := funex
 
 /--
 A pure proposition `P : Prop` embedded into `SPred`.
-Prefer to use idiom bracket notation `⌜P⌝.
+Prefer to use notation `⌜P⌝`.
 -/
 def pure {σs : List (Type u)} (P : Prop) : SPred σs := match σs with
   | [] => ULift.up P
@@ -50,7 +54,13 @@ def pure {σs : List (Type u)} (P : Prop) : SPred σs := match σs with
 theorem pure_nil : pure (σs:=[]) P = ULift.up P := rfl
 theorem pure_cons : pure (σs:=σ::σs) P = fun _ => pure P := rfl
 
-/-- Entailment in `SPred`. -/
+/--
+Entailment in `SPred`.
+
+One predicate `P` entails another predicate `Q` if `Q` is true in every state in which `P` is true.
+Unlike implication (`SPred.imp`), entailment is not itself an `SPred`, but is instead an ordinary
+proposition.
+-/
 def entails {σs : List (Type u)} (P Q : SPred σs) : Prop := match σs with
   | [] => P.down → Q.down
   | σ :: _ => ∀ (s : σ), entails (P s) (Q s)
@@ -62,7 +72,12 @@ theorem entails_cons_intro {P Q : SPred (σ::σs)} : (∀ s, entails (P s) (Q s)
 
 -- Reducibility of entails must be semi-reducible so that entails_refl is useful for rfl
 
-/-- Equivalence relation on `SPred`. Convert to `Eq` via `bientails.to_eq`. -/
+/--
+Logical equivalence of `SPred`.
+
+Logically equivalent predicates are equal. Use `SPred.bientails.to_eq` to convert bi-entailment to
+equality.
+-/
 def bientails {σs : List (Type u)} (P Q : SPred σs) : Prop := match σs with
   | [] => P.down ↔ Q.down
   | σ :: _ => ∀ (s : σ), bientails (P s) (Q s)
@@ -70,35 +85,40 @@ def bientails {σs : List (Type u)} (P Q : SPred σs) : Prop := match σs with
 theorem bientails_cons {P Q : SPred (σ::σs)} : bientails P Q = (∀ s, bientails (P s) (Q s)) := rfl
 theorem bientails_cons_intro {P Q : SPred (σ::σs)} : (∀ s, bientails (P s) (Q s)) → bientails P Q := by simp only [bientails_cons, imp_self]
 
-/-- Conjunction in `SPred`. -/
+/-- Conjunction in `SPred`: states that satisfy `P` and satisfy `Q` satisfy `spred(P ∧ Q)`. -/
 def and {σs : List (Type u)} (P Q : SPred σs) : SPred σs := match σs with
   | [] => ⟨P.down ∧ Q.down⟩
   | σ :: _ => fun (s : σ) => and (P s) (Q s)
 @[simp, grind =] theorem and_nil {P Q : SPred []} : and P Q = ⟨P.down ∧ Q.down⟩ := rfl
 @[simp, grind =] theorem and_cons {P Q : SPred (σ::σs)} : and P Q s = and (P s) (Q s) := rfl
 
-/-- Disjunction in `SPred`. -/
+/-- Disjunction in `SPred`: states that either satisfy `P` or satisfy `Q` satisfy `spred(P ∨ Q)`. -/
 def or {σs : List (Type u)} (P Q : SPred σs) : SPred σs := match σs with
   | [] => ⟨P.down ∨ Q.down⟩
   | σ :: _ => fun (s : σ) => or (P s) (Q s)
 @[simp, grind =] theorem or_nil {P Q : SPred []} : or P Q = ⟨P.down ∨ Q.down⟩ := rfl
 @[simp, grind =] theorem or_cons {P Q : SPred (σ::σs)} : or P Q s = or (P s) (Q s) := rfl
 
-/-- Negation in `SPred`. -/
+/-- Negation in `SPred`: states that do not satisfy `P` satisfy `spred(¬ P)`. -/
 def not {σs : List (Type u)} (P : SPred σs) : SPred σs := match σs with
   | [] => ⟨¬ P.down⟩
   | σ :: _ => fun (s : σ) => not (P s)
 @[simp, grind =] theorem not_nil {P : SPred []} : not P = ⟨¬ P.down⟩ := rfl
 @[simp, grind =] theorem not_cons {P : SPred (σ::σs)} : not P s = not (P s) := rfl
 
-/-- Implication in `SPred`. -/
+/--
+Implication in `SPred`: states that satisfy `Q` whenever they satisfy `P` satisfy `spred(P → Q)`.
+-/
 def imp {σs : List (Type u)} (P Q : SPred σs) : SPred σs := match σs with
   | [] => ⟨P.down → Q.down⟩
   | σ :: _ => fun (s : σ) => imp (P s) (Q s)
 @[simp, grind =] theorem imp_nil {P Q : SPred []} : imp P Q = ⟨P.down → Q.down⟩ := rfl
 @[simp, grind =] theorem imp_cons {P Q : SPred (σ::σs)} : imp P Q s = imp (P s) (Q s) := rfl
 
-/-- Biconditional in `SPred`. -/
+/--
+Biimplication in `SPred`: states that either satisfy both `P` and `Q` or satisfy neither satisfy
+`spred(P ↔ Q)`.
+-/
 def iff {σs : List (Type u)} (P Q : SPred σs) : SPred σs := match σs with
   | [] => ⟨P.down ↔ Q.down⟩
   | σ :: _ => fun (s : σ) => iff (P s) (Q s)
@@ -119,7 +139,10 @@ def «forall» {α : Sort u} {σs : List (Type v)} (P : α → SPred σs) : SPre
 @[simp, grind =] theorem forall_nil {α} {P : α → SPred []} : «forall» P = ⟨∀ a, (P a).down⟩ := rfl
 @[simp, grind =] theorem forall_cons {α} {P : α → SPred (σ::σs)} : «forall» P s = «forall» (fun a => P a s) := rfl
 
-/-- Conjunction of a list of `SPred`. -/
+/--
+Conjunction of a list of stateful predicates. A state satisfies `conjunction env` if it satisfies
+all predicates in `env`.
+-/
 def conjunction {σs : List (Type u)} (env : List (SPred σs)) : SPred σs := match env with
   | [] => pure True
   | P::env => P.and (conjunction env)
diff --git a/src/Std/Do/SPred/SVal.lean b/src/Std/Do/SPred/SVal.lean
index b292de5919e5..0cb339ba57d5 100644
--- a/src/Std/Do/SPred/SVal.lean
+++ b/src/Std/Do/SPred/SVal.lean
@@ -11,21 +11,26 @@ import Init.SimpLemmas
 
 @[expose] public section
 
+set_option linter.missingDocs true
+
 /-! # State-indexed values -/
 
 namespace Std.Do
 
 /--
-  A value indexed by a curried tuple of states.
-  ```
-  example : SVal [Nat, Bool] String = (Nat → Bool → String) := rfl
-  ```
+A value indexed by a curried tuple of states.
+
+Example:
+```
+example : SVal [Nat, Bool] String = (Nat → Bool → String) := rfl
+```
 -/
 abbrev SVal (σs : List (Type u)) (α : Type u) : Type u := match σs with
   | [] => α
   | σ :: σs => σ → SVal σs α
 
-/- Note about the reducibility of SVal:
+/-
+Note about the reducibility of SVal:
 We need SVal to be reducible, otherwise type inference fails for `Triple`.
 This is tracked in #8074. There is a fix in #9015, but it regresses Mathlib.
 -/
@@ -43,14 +48,14 @@ instance : Inhabited (StateTuple []) where
 instance [Inhabited σ] [Inhabited (StateTuple σs)] : Inhabited (StateTuple (σ :: σs)) where
   default := (default, default)
 
-/-- Curry a function taking a `StateTuple` into an `SVal`. -/
+/-- Curries a function taking a `StateTuple` into an `SVal`. -/
 def curry {σs : List (Type u)} (f : StateTuple σs → α) : SVal σs α := match σs with
   | [] => f ⟨⟩
   | _ :: _ => fun s => curry (fun s' => f (s, s'))
 @[simp, grind =] theorem curry_nil {f : StateTuple [] → α} : curry f = f ⟨⟩ := rfl
 @[simp, grind =] theorem curry_cons {σ : Type u} {σs : List (Type u)} {f : StateTuple (σ::σs) → α} {s : σ} : curry f s = curry (fun s' => f (s, s')) := rfl
 
-/-- Uncurry an `SVal` into a function taking a `StateTuple`. -/
+/-- Uncurries an `SVal` into a function taking a `StateTuple`. -/
 def uncurry {σs : List (Type u)} (f : SVal σs α) : StateTuple σs → α := match σs with
   | [] => fun _ => f
   | _ :: _ => fun (s, t) => uncurry (f s) t
@@ -63,7 +68,12 @@ def uncurry {σs : List (Type u)} (f : SVal σs α) : StateTuple σs → α := m
 instance [Inhabited α] : Inhabited (SVal σs α) where
   default := curry fun _ => default
 
+/--
+Auxiliary type class used by `SVal.getThe` to construct a projection from a list of state types to
+one of the component states.
+-/
 class GetTy (σ : Type u) (σs : List (Type u)) where
+  /-- A projection from the types `σs` of type `σ`. -/
   get : SVal σs σ
 
 instance : GetTy σ (σ :: σs) where
@@ -72,7 +82,7 @@ instance : GetTy σ (σ :: σs) where
 instance [GetTy σ₁ σs] : GetTy σ₁ (σ₂ :: σs) where
   get := fun _ => GetTy.get
 
-/-- Get the top-most state of type `σ` from an `SVal`. -/
+/-- Gets the top-most state of type `σ` from an `SVal`. -/
 def getThe {σs : List (Type u)} (σ : Type u) [GetTy σ σs] : SVal σs σ := GetTy.get
 @[simp, grind =] theorem getThe_here {σs : List (Type u)} (σ : Type u) (s : σ) : getThe (σs := σ::σs) σ s = curry (fun _ => s) := rfl
 @[simp, grind =] theorem getThe_there {σs : List (Type u)} [GetTy σ σs] (σ' : Type u) (s : σ') : getThe (σs := σ'::σs) σ s = getThe (σs := σs) σ := rfl
diff --git a/src/Std/Do/Triple.lean b/src/Std/Do/Triple.lean
index 85362ca900d1..14efbb16edc4 100644
--- a/src/Std/Do/Triple.lean
+++ b/src/Std/Do/Triple.lean
@@ -8,3 +8,5 @@ module
 prelude
 public import Std.Do.Triple.Basic
 public import Std.Do.Triple.SpecLemmas
+
+set_option linter.missingDocs true
diff --git a/src/Std/Do/Triple/Basic.lean b/src/Std/Do/Triple/Basic.lean
index 6b681b485fbe..1108b71d3905 100644
--- a/src/Std/Do/Triple/Basic.lean
+++ b/src/Std/Do/Triple/Basic.lean
@@ -9,6 +9,8 @@ prelude
 public import Std.Do.WP
 meta import Std.Do.SPred.Notation
 
+set_option linter.missingDocs true
+
 @[expose] public section
 
 /-!
@@ -27,11 +29,11 @@ universe u v
 variable {m : Type u → Type v} {ps : PostShape.{u}}
 
 /--
-  A Hoare triple for reasoning about monadic programs.
-  A proof for `Triple x P Q` is a *specification* for `x`:
-  If assertion `P` holds before `x`, then postcondition `Q` holds after running `x`.
+A Hoare triple for reasoning about monadic programs. A Hoare triple `Triple x P Q` is a
+*specification* for `x`: if assertion `P` holds before `x`, then postcondition `Q` holds after
+running `x`.
 
-  `⦃P⦄ x ⦃Q⦄` is convenient syntax for `Triple x P Q`.
+`⦃P⦄ x ⦃Q⦄` is convenient syntax for `Triple x P Q`.
 -/
 def Triple [WP m ps] {α : Type u} (x : m α) (P : Assertion ps) (Q : PostCond α ps) : Prop :=
   P ⊢ₛ wp⟦x⟧ Q
@@ -39,6 +41,9 @@ def Triple [WP m ps] {α : Type u} (x : m α) (P : Assertion ps) (Q : PostCond 
 @[inherit_doc Std.Do.Triple]
 scoped syntax:lead (name := triple) "⦃" term "⦄ " term:lead " ⦃" term "⦄" : term
 
+/--
+Unexpands Hoare triples to their high-level syntax during pretty printing.
+-/
 @[app_unexpander Triple]
 meta def unexpandTriple : Lean.PrettyPrinter.Unexpander
   | `($_ $x $P $Q) => do
diff --git a/src/Std/Do/Triple/SpecLemmas.lean b/src/Std/Do/Triple/SpecLemmas.lean
index 91c8019c3dd3..42de98cf8fbe 100644
--- a/src/Std/Do/Triple/SpecLemmas.lean
+++ b/src/Std/Do/Triple/SpecLemmas.lean
@@ -16,6 +16,8 @@ public import Init.Data.Iterators.ToIterator
 -- Without it, adding the `spec` attribute for `instMonadLiftTOfMonadLift` will fail.
 public import Init.Data.Iterators.Lemmas.Combinators.FilterMap
 
+set_option linter.missingDocs true
+
 @[expose] public section
 
 /-!
@@ -26,6 +28,9 @@ This module contains Hoare triple specifications for some functions in Core.
 
 namespace Std.Range
 
+/--
+Converts a range to the list of all numbers in the range.
+-/
 abbrev toList (r : Std.Range) : List Nat :=
   List.range' r.start ((r.stop - r.start + r.step - 1) / r.step) r.step
 
@@ -33,19 +38,61 @@ end Std.Range
 
 namespace List
 
+/--
+A pointer at a specific location in a list. List cursors are used in loop invariants for the
+`mvcgen` tactic.
+
+Moving the cursor to the left or right takes time linear in the current position of the cursor, so
+this data structure is not appropriate for run-time code.
+-/
 @[ext]
 structure Cursor {α : Type u} (l : List α) : Type u where
+  /--
+  The elements before to the current position in the list.
+  -/
   «prefix» : List α
+  /--
+  The elements starting at the current position. If the position is after the last element of the
+  list, then the suffix is empty; otherwise, the first element of the suffix is the current element
+  that the cursor points to.
+  -/
   suffix : List α
+  /-- Appending the prefix to the suffix yields the original list. -/
   property : «prefix» ++ suffix = l
 
+/--
+Creates a cursor at position `n` in the list `l`.
+The prefix contains the first `n` elements, and the suffix contains the remaining elements.
+If `n` is larger than the length of the list, the cursor is positioned at the end of the list.
+-/
 def Cursor.at (l : List α) (n : Nat) : Cursor l := ⟨l.take n, l.drop n, by simp⟩
+
+/--
+Creates a cursor at the beginning of the list (position 0).
+The prefix is empty and the suffix is the entire list.
+-/
 abbrev Cursor.begin (l : List α) : Cursor l := .at l 0
+
+/--
+Creates a cursor at the end of the list.
+The prefix is the entire list and the suffix is empty.
+-/
 abbrev Cursor.end (l : List α) : Cursor l := .at l l.length
 
+/--
+Returns the element at the current cursor position.
+
+Requires that is a current element: the suffix must be non-empty, so the cursor is not at the end of
+the list.
+-/
 def Cursor.current {α} {l : List α} (c : Cursor l) (h : 0 < c.suffix.length := by get_elem_tactic) : α :=
   c.suffix[0]'(by simp [h])
 
+/--
+Advances the cursor by one position, moving the current element from the suffix to the prefix.
+
+Requires that the cursor is not already at the end of the list.
+-/
 def Cursor.tail (s : Cursor l) (h : 0 < s.suffix.length := by get_elem_tactic) : Cursor l :=
   { «prefix» := s.prefix ++ [s.current]
   , suffix := s.suffix.tail
diff --git a/src/Std/Do/WP.lean b/src/Std/Do/WP.lean
index 1ae1260e528c..0426aadc2fa8 100644
--- a/src/Std/Do/WP.lean
+++ b/src/Std/Do/WP.lean
@@ -9,3 +9,5 @@ prelude
 public import Std.Do.WP.Basic
 public import Std.Do.WP.Monad
 public import Std.Do.WP.SimpLemmas
+
+set_option linter.missingDocs true
diff --git a/src/Std/Do/WP/Basic.lean b/src/Std/Do/WP/Basic.lean
index 4381c48aa1af..65e6dae28617 100644
--- a/src/Std/Do/WP/Basic.lean
+++ b/src/Std/Do/WP/Basic.lean
@@ -10,6 +10,8 @@ public import Std.Do.PredTrans
 
 @[expose] public section
 
+set_option linter.missingDocs true
+
 /-!
 # Weakest precondition interpretation
 
@@ -44,9 +46,10 @@ universe u v
 variable {m : Type u → Type v}
 
 /--
-  A weakest precondition interpretation of a monadic program `x : m α` in terms of a
-  predicate transformer `PredTrans ps α`.
-  The monad `m` determines `ps : PostShape`. See the module comment for more details.
+A weakest precondition interpretation of a monadic program `x : m α` in terms of a predicate
+transformer `PredTrans ps α`. The monad `m` determines `ps : PostShape`.
+
+For practical reasoning, an instance of `WPMonad m ps` is typically needed in addition to `WP m ps`.
 -/
 class WP (m : Type u → Type v) (ps : outParam PostShape.{u}) where
   /-- Interpret a monadic program `x : m α` in terms of a predicate transformer `PredTrans ps α`. -/
@@ -60,6 +63,9 @@ macro_rules
   | `(wp⟦$x:term⟧) => `((WP.wp $x).apply)
   | `(wp⟦$x:term : $ty⟧) => `((WP.wp ($x : $ty)).apply)
 
+/--
+An unexpander for the `wp⟦...⟧` notation, causing it to be shown correctly in the pretty printer.
+-/
 @[app_unexpander PredTrans.apply]
 protected meta def unexpandWP : Lean.PrettyPrinter.Unexpander
   | `($_ $e) => match e with
diff --git a/src/Std/Do/WP/Monad.lean b/src/Std/Do/WP/Monad.lean
index f3b69583466e..99d8bd173f15 100644
--- a/src/Std/Do/WP/Monad.lean
+++ b/src/Std/Do/WP/Monad.lean
@@ -11,6 +11,8 @@ import all Std.Do.WP.Basic
 
 @[expose] public section
 
+set_option linter.missingDocs true
+
 /-!
 # Monad morphisms and weakest precondition interpretations
 
@@ -24,7 +26,12 @@ universe u v
 variable {m : Type u → Type v} {ps : PostShape.{u}}
 
 /--
-  A `WP` that is also a monad morphism, preserving `pure` and `bind`. (They all are.)
+A monad with weakest preconditions (`WP`) that is also a monad morphism, preserving `pure` and
+`bind`.
+
+In practice, `mvcgen` is not useful for reasoning about programs in a monad that is without a
+`WPMonad` instance. The specification lemmas for `Pure.pure` and `Bind.bind`, as well as those for
+operators like `Functor.map`, require that their monad have a `WPMonad` instance.
 -/
 class WPMonad (m : Type u → Type v) (ps : outParam PostShape.{u}) [Monad m]
   extends LawfulMonad m, WP m ps where
diff --git a/src/Std/Do/WP/SimpLemmas.lean b/src/Std/Do/WP/SimpLemmas.lean
index d5672bd1d492..34371b41cfd6 100644
--- a/src/Std/Do/WP/SimpLemmas.lean
+++ b/src/Std/Do/WP/SimpLemmas.lean
@@ -10,6 +10,8 @@ public import Std.Do.WP.Monad
 
 @[expose] public section
 
+set_option linter.missingDocs true
+
 /-!
 # Simp lemmas for working with weakest preconditions