diff --git a/RandomDo/Measurable.lean b/RandomDo/Measurable.lean
index 94ca927..7887e6a 100644
--- a/RandomDo/Measurable.lean
+++ b/RandomDo/Measurable.lean
@@ -31,6 +31,7 @@ open MeasureTheory Set
 
 variable {α : Type*} [MeasurableSpace α]
 
+/-- Lists are measurably equivalent to the sigma type of tuples of a given length. -/
 def List.measurableEquivSigmaTuple : List α ≃ᵐ Σ n, Fin n → α where
   toFun := List.equivSigmaTuple
   invFun := List.equivSigmaTuple.symm
@@ -102,6 +103,7 @@ lemma Vector.measurableSpace_eq_comap {n : ℕ} :
           (MeasurableSpace.comap List.ofFn inferInstance) := MeasurableSpace.comap_comp.symm
     _ = _ := by rw [(measurableEmbedding_ofFn n).comap_eq]
 
+/-- Vectors are equivalent to tuples of a given length. -/
 def Vector.measurableEquivTuple {n : ℕ} : Vector α n ≃ᵐ (Fin n → α) where
   toFun v := fun i ↦ v[i]
   invFun := .ofFn
diff --git a/RandomDo/Monad/Instances.lean b/RandomDo/Monad/Instances.lean
index c633f3c..87afea9 100644
--- a/RandomDo/Monad/Instances.lean
+++ b/RandomDo/Monad/Instances.lean
@@ -21,7 +21,7 @@ universe u v w
 
 /-- A (core) monad automatically defines a (not necessarily lawful) measurable space monad by
 forgetting the measurable space argument. -/
-def Monad.toMeasurableSpaceMonad (m : Type u → Type v) [Monad m] (α : Type u) [MeasurableSpace α] :
+def Monad.toMeasurableSpaceMonad (m : Type u → Type v) (α : Type u) [_mα : MeasurableSpace α] :
     Type v := m α
 
 instance {m : Type u → Type v} [Monad m] :
@@ -54,11 +54,13 @@ section RandomM
 
 open Function
 
+/-- A monad for random number generation. -/
 structure RandomM (Ω : Type w) [MeasurableSpace Ω] (P : Measure Ω)
     (α : Type u) [MeasurableSpace α] where
   sample : Ω → α × Ω
   measurePreserving : MeasurePreserving sample P ((Measure.map (Prod.fst ∘ sample) P).prod P)
 
+/-- TODO -/
 abbrev SampleM (Ω : Type w) [MeasurableSpace Ω] (P : Measure Ω) :=
   RandomM (ℕ → Ω) (Measure.infinitePi fun _ : ℕ ↦ P)
 
diff --git a/RandomDo/Monad/MeasurableSpace.lean b/RandomDo/Monad/MeasurableSpace.lean
index 7a7da1a..9b5fa7c 100644
--- a/RandomDo/Monad/MeasurableSpace.lean
+++ b/RandomDo/Monad/MeasurableSpace.lean
@@ -65,6 +65,8 @@ The `mPure` function is overloaded via `MeasurableSpacePure` instances.
 `MeasurableSpacePure` is typically accessed via `MeasurableSpaceMonad` instances, which extend it.
 -/
 class MeasurableSpacePure (f : (α : Type u) → [MeasurableSpace α] → Type v) where
+  /-- Given `a : α` where `α` has a `MeasurableSpace` instance, `mPure a : f α` represents an
+  action that does nothing and returns a -/
   mPure {α : Type u} [MeasurableSpace α] : α → f α
 
 /--
diff --git a/RandomDo/Monad/Notation.lean b/RandomDo/Monad/Notation.lean
index 1943765..7d06205 100644
--- a/RandomDo/Monad/Notation.lean
+++ b/RandomDo/Monad/Notation.lean
@@ -63,6 +63,7 @@ def randOps : DoOps := { DoOps.default with
     return mkApp2 m α σ
   }
 
+/-- The `do` notation for writing monadic programs depending on a `MeasurableSpace` instance. -/
 syntax (name := randKind) "rdo" doSeq : term
 
 /-- Define `rdo` notation elaborator. -/
diff --git a/RandomDo/Tactic/Examples.lean b/RandomDo/Tactic/Examples.lean
index 56df367..e702087 100644
--- a/RandomDo/Tactic/Examples.lean
+++ b/RandomDo/Tactic/Examples.lean
@@ -155,4 +155,8 @@ attribute[fun_prop] ProbabilityTheory.Kernel.measurable_coe
 example : Measurable fun a => κ a s := by
   fun_prop (disch := measurability)
 
+/- The programs above are examples of what `rdo` and `is_markov` do, not an API: `docBlame` is
+told not to ask them for documentation. -/
+attribute [nolint docBlame] test1 test2 test3 test4 test5 thompson Vector.v_equiv
+
 end