diff --git a/src/Lean/Elab/Print.lean b/src/Lean/Elab/Print.lean
index e0506641fe..505cfa9397 100644
--- a/src/Lean/Elab/Print.lean
+++ b/src/Lean/Elab/Print.lean
@@ -56,6 +56,7 @@ private def printQuot (kind : QuotKind) (id : Name) (levelParams : List Name) (t
 private def printInduct (id : Name) (levelParams : List Name) (numParams : Nat) (numIndices : Nat) (type : Expr)
     (ctors : List Name) (isUnsafe : Bool) : CommandElabM Unit := do
   let mut m ← mkHeader' "inductive" id levelParams type isUnsafe
+  m := m ++ Format.line ++ "number of parameters: " ++ toString numParams
   m := m ++ Format.line ++ "constructors:"
   for ctor in ctors do
     let cinfo ← getConstInfo ctor
diff --git a/tests/lean/diamond1.lean.expected.out b/tests/lean/diamond1.lean.expected.out
index c46ed88a08..0a21f210b7 100644
--- a/tests/lean/diamond1.lean.expected.out
+++ b/tests/lean/diamond1.lean.expected.out
@@ -3,6 +3,7 @@ diamond1.lean:11:40-11:45: error: parent field type mismatch, field 'a' from par
 but is expected to have type
   α : Type
 inductive Foo : Type → Type
+number of parameters: 1
 constructors:
 Foo.mk : {α : Type} → Bar (α → α) → (Bool → α) → Nat → Foo α
 def f : Nat → Foo Nat :=
diff --git a/tests/lean/diamond8.lean.expected.out b/tests/lean/diamond8.lean.expected.out
index d08a5fd62c..12855d268e 100644
--- a/tests/lean/diamond8.lean.expected.out
+++ b/tests/lean/diamond8.lean.expected.out
@@ -1,3 +1,4 @@
 inductive Semiring.{u} : Type u → Type u
+number of parameters: 1
 constructors:
 Semiring.mk : {R : Type u} → [toAddCommMonoid : AddCommMonoid R] → [toMonoid : Monoid R] → Semiring R
diff --git a/tests/lean/structAutoBound.lean.expected.out b/tests/lean/structAutoBound.lean.expected.out
index ecc433737e..0278987b6b 100644
--- a/tests/lean/structAutoBound.lean.expected.out
+++ b/tests/lean/structAutoBound.lean.expected.out
@@ -1,8 +1,10 @@
 inductive Foo.{v, u_1} : {α : Sort u_1} → (α → Type v) → Sort (max u_1 (v + 1))
+number of parameters: 2
 constructors:
 Foo.mk : {α : Sort u_1} → {β : α → Type v} → (a : α) → β a → Foo β
 structAutoBound.lean:9:15-9:16: error: a universe level named 'u' has already been declared
 inductive Boo.{u, v} : Type u → Type v → Type (max u v)
+number of parameters: 2
 constructors:
 Boo.mk : {α : Type u} → {β : Type v} → α → β → Boo α β
 structAutoBound.lean:18:0-20:7: error: unused universe parameter 'w'