diff --git a/tests/lean/run/derivingToExpr.lean b/tests/lean/run/derivingToExpr.lean
new file mode 100644
index 000000000000..c3504075ccb1
--- /dev/null
+++ b/tests/lean/run/derivingToExpr.lean
@@ -0,0 +1,22 @@
+import Lean.Elab.Deriving.ToExpr
+
+open Lean (ToExpr)
+
+-- Test with a universe polymporphic type parameter
+inductive Option' (α : Type u)
+  | some (a : α)
+  | none
+  deriving ToExpr
+
+-- Test with recursive type
+inductive List' (α : Type u)
+  | cons (a : α) (as : List' α)
+  | nil
+  deriving ToExpr
+
+-- Test without (universe) auto implicit
+set_option autoImplicit false in
+inductive ExplicitList'.{u} (α : Type u)
+  | cons (a : α) (as : List' α)
+  | nil
+  deriving ToExpr