diff --git a/doc/examples/interp.lean b/doc/examples/interp.lean
index f32e8ed4c8..bf99e4a1d0 100644
--- a/doc/examples/interp.lean
+++ b/doc/examples/interp.lean
@@ -22,7 +22,7 @@ inductive Vector (α : Type u) : Nat → Type u
   | cons : α → Vector α n → Vector α (n+1)
 
 /-|
-We can overload the `List.cons` notation `::` and use it to create `Vector`s.
+We can overload the `List.cons` notation `::` and use it to create `Vector`\ s.
 -/
 infix:67 " :: " => Vector.cons