diff --git a/src/Lean/Declaration.lean b/src/Lean/Declaration.lean
index 8fbbc5c1dc..bdf328aeb5 100644
--- a/src/Lean/Declaration.lean
+++ b/src/Lean/Declaration.lean
@@ -223,7 +223,7 @@ def mkInductiveValEx (name : Name) (levelParams : List Name) (type : Expr) (numP
 @[export lean_inductive_val_is_reflexive] def InductiveVal.isReflexiveEx (v : InductiveVal) : Bool := v.isReflexive
 @[export lean_inductive_val_is_nested] def InductiveVal.isNestedEx (v : InductiveVal) : Bool := v.isNested
 
-def InductiveVal.nctors (v : InductiveVal) : Nat := v.ctors.length
+def InductiveVal.numCtors (v : InductiveVal) : Nat := v.ctors.length
 
 structure ConstructorVal extends ConstantVal where
   induct  : Name    -- Inductive Type this Constructor is a member of
diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index d303310c33..46dd7d4c08 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -26,7 +26,7 @@ private def isDefEqEtaStruct (a b : Expr) : MetaM Bool :=
       return false
     else
       let inductVal ← getConstInfoInduct ctorVal.induct
-      if inductVal.nctors != 1 || inductVal.numIndices != 0 || inductVal.isRec then
+      if inductVal.numCtors != 1 || inductVal.numIndices != 0 || inductVal.isRec then
         trace[Meta.isDefEq.eta.struct] "failed, type is not a structure{indentExpr b}"
         return false
       else if (← isDefEq (← inferType a) (← inferType b)) then