diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index 0bf5cfe377..fc6b780fe1 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -622,11 +622,11 @@ def delabProjectionApp : Delab := whenPPOption getPPStructureProjections $ do
   guard $ !info.fromClass
   -- projection function should be fully applied (#struct params + 1 instance parameter)
   -- TODO: support over-application
-  guard $ e.getAppNumArgs == info.nparams + 1
+  guard $ e.getAppNumArgs == info.numParams + 1
   -- If pp.explicit is true, and the structure has parameters, we should not
   -- use field notation because we will not be able to see the parameters.
   let expl ← getPPOption getPPExplicit
-  guard $ !expl || info.nparams == 0
+  guard $ !expl || info.numParams == 0
   let appStx ← withAppArg delab
   `($(appStx).$(mkIdent f):ident)
 
diff --git a/src/Lean/ProjFns.lean b/src/Lean/ProjFns.lean
index ebb04e0184..9f2f866cea 100644
--- a/src/Lean/ProjFns.lean
+++ b/src/Lean/ProjFns.lean
@@ -11,24 +11,23 @@ namespace Lean
    for each field. This structure caches information about these auxiliary definitions. -/
 structure ProjectionFunctionInfo where
   ctorName : Name  -- Constructor associated with the auxiliary projection function.
-  nparams : Nat    -- Number of parameters in the structure
+  numParams : Nat  -- Number of parameters in the structure
   i : Nat          -- The field index associated with the auxiliary projection function.
   fromClass : Bool -- `true` if the structure is a class
+  deriving Inhabited
 
 @[export lean_mk_projection_info]
-def mkProjectionInfoEx (ctorName : Name) (nparams : Nat) (i : Nat) (fromClass : Bool) : ProjectionFunctionInfo :=
-  {ctorName := ctorName, nparams := nparams, i := i, fromClass := fromClass }
+def mkProjectionInfoEx (ctorName : Name) (numParams : Nat) (i : Nat) (fromClass : Bool) : ProjectionFunctionInfo :=
+  { ctorName, numParams, i, fromClass }
 @[export lean_projection_info_from_class]
-  def ProjectionFunctionInfo.fromClassEx (info : ProjectionFunctionInfo) : Bool := info.fromClass
-
-instance : Inhabited ProjectionFunctionInfo :=
-  ⟨{ ctorName := arbitrary, nparams := arbitrary, i := 0, fromClass := false }⟩
+def ProjectionFunctionInfo.fromClassEx (info : ProjectionFunctionInfo) : Bool :=
+  info.fromClass
 
 builtin_initialize projectionFnInfoExt : MapDeclarationExtension ProjectionFunctionInfo ← mkMapDeclarationExtension `projinfo
 
 @[export lean_add_projection_info]
-def addProjectionFnInfo (env : Environment) (projName : Name) (ctorName : Name) (nparams : Nat) (i : Nat) (fromClass : Bool) : Environment :=
-  projectionFnInfoExt.insert env projName { ctorName := ctorName, nparams := nparams, i := i, fromClass := fromClass }
+def addProjectionFnInfo (env : Environment) (projName : Name) (ctorName : Name) (numParams : Nat) (i : Nat) (fromClass : Bool) : Environment :=
+  projectionFnInfoExt.insert env projName { ctorName, numParams, i, fromClass }
 
 namespace Environment