diff --git a/tests/lean/docStr.lean b/tests/lean/docStr.lean
index f4fd62ad3a..053420b33d 100644
--- a/tests/lean/docStr.lean
+++ b/tests/lean/docStr.lean
@@ -67,5 +67,8 @@ def printDocStrings : MetaM Unit := do
   printDocString `f.foo
   printDocString `g
   printDocString `g.foo
+  printDocString `optParam
+  printDocString `namedPattern
+  printDocString `Lean.Meta.forallTelescopeReducing
 
 #eval printDocStrings
diff --git a/tests/lean/docStr.lean.expected.out b/tests/lean/docStr.lean.expected.out
index 181d35bc24..bdf600b41e 100644
--- a/tests/lean/docStr.lean.expected.out
+++ b/tests/lean/docStr.lean.expected.out
@@ -15,3 +15,6 @@ doc string for 'f' is not available
 "let rec documentation at f "
 doc string for 'g' is not available
 "let rec documentation at g "
+"Gadget for optional parameter support. "
+"Auxiliary Declaration used to implement the named patterns `x@p` "
+"Similar to `forallTelescope`, but given `type` of the form `forall xs, A`,\n  it reduces `A` and continues bulding the telescope if it is a `forall`. "