chore: naming convention

src/Lean/Declaration.lean

@@ -334,7 +334,7 @@ def isUnsafe : ConstantInfo → Bool
 def name (d : ConstantInfo) : Name :=
   d.toConstantVal.name
 
-def lparams (d : ConstantInfo) : List Name :=
+def levelParams (d : ConstantInfo) : List Name :=
   d.toConstantVal.levelParams
 
 def type (d : ConstantInfo) : Expr :=

src/Lean/Elab/StructInst.lean

@@ -665,7 +665,7 @@ partial def mkDefaultValueAux? (struct : Struct) : Expr → TermElabM (Option Ex
 
 def mkDefaultValue? (struct : Struct) (cinfo : ConstantInfo) : TermElabM (Option Expr) :=
   withRef struct.ref do
-  let us ← cinfo.lparams.mapM fun _ => mkFreshLevelMVar
+  let us ← cinfo.levelParams.mapM fun _ => mkFreshLevelMVar
   mkDefaultValueAux? struct (cinfo.instantiateValueLevelParams us)
 
 /-- If `e` is a projection function of one of the given structures, then reduce it -/

src/Lean/Elab/SyntheticMVars.lean

@@ -138,7 +138,7 @@ private def synthesizeSyntheticMVarsStep (postponeOnError : Bool) (runTactics :
 private def tryToSynthesizeUsingDefaultInstance (mvarId : MVarId) (defaultInstance : Name) : MetaM (Option (List SyntheticMVarDecl)) :=
   commitWhenSome? do
     let constInfo ← getConstInfo defaultInstance
-    let candidate := Lean.mkConst defaultInstance (← mkFreshLevelMVars constInfo.lparams.length)
+    let candidate := Lean.mkConst defaultInstance (← mkFreshLevelMVars constInfo.levelParams.length)
     let (mvars, bis, _) ← forallMetaTelescopeReducing (← inferType candidate)
     let candidate := mkAppN candidate mvars
     trace[Elab.resume]! "trying default instance for {mkMVar mvarId} := {candidate}"

src/Lean/Elab/Term.lean

@@ -1241,10 +1241,10 @@ def mkFreshLevelMVars (num : Nat) : MetaM (List Level) :=
   parameters than `explicitLevels`. -/
 def mkConst (constName : Name) (explicitLevels : List Level := []) : TermElabM Expr := do
   let cinfo ← getConstInfo constName
-  if explicitLevels.length > cinfo.lparams.length then
+  if explicitLevels.length > cinfo.levelParams.length then
     throwError "too many explicit universe levels"
   else
-    let numMissingLevels := cinfo.lparams.length - explicitLevels.length
+    let numMissingLevels := cinfo.levelParams.length - explicitLevels.length
     let us ← mkFreshLevelMVars numMissingLevels
     pure $ Lean.mkConst constName (explicitLevels ++ us)
 

src/Lean/Meta/AppBuilder.lean

@@ -216,7 +216,7 @@ private partial def mkAppMArgs (f : Expr) (fType : Expr) (xs : Array Expr) : Met
 
 private def mkFun (constName : Name) : MetaM (Expr × Expr) := do
   let cinfo ← getConstInfo constName
-  let us ← cinfo.lparams.mapM fun _ => mkFreshLevelMVar
+  let us ← cinfo.levelParams.mapM fun _ => mkFreshLevelMVar
   let f := mkConst constName us
   let fType := cinfo.instantiateTypeLevelParams us
   return (f, fType)

src/Lean/Meta/Check.lean

@@ -26,7 +26,7 @@ def throwLetTypeMismatchMessage {α} (fvarId : FVarId) : MetaM α := do
 
 private def checkConstant (constName : Name) (us : List Level) : MetaM Unit := do
   let cinfo ← getConstInfo constName
-  unless us.length == cinfo.lparams.length do
+  unless us.length == cinfo.levelParams.length do
     throwIncorrectNumberOfLevels constName us
 
 private def getFunctionDomain (f : Expr) : MetaM (Expr × BinderInfo) := do

src/Lean/Meta/InferType.lean

@@ -88,8 +88,8 @@ def throwIncorrectNumberOfLevels {α} (constName : Name) (us : List Level) : Met
 
 private def inferConstType (c : Name) (us : List Level) : MetaM Expr := do
   let cinfo ← getConstInfo c
-  if cinfo.lparams.length == us.length then
-    pure $ cinfo.instantiateTypeLevelParams us
+  if cinfo.levelParams.length == us.length then
+    return cinfo.instantiateTypeLevelParams us
   else
     throwIncorrectNumberOfLevels c us
 

src/Lean/Meta/Instances.lean

@@ -51,7 +51,7 @@ private def mkInstanceKey (e : Expr) : MetaM (Array DiscrTree.Key) := do
 
 def addInstance (declName : Name) (attrKind : AttributeKind) (prio : Nat) : MetaM Unit := do
   let cinfo ← getConstInfo declName
-  let c := mkConst declName (cinfo.lparams.map mkLevelParam)
+  let c := mkConst declName (cinfo.levelParams.map mkLevelParam)
   let keys ← mkInstanceKey c
   instanceExtension.add { keys := keys, val := c, priority := prio, globalName? := declName } attrKind
 

src/Lean/Meta/RecursorInfo.lean

@@ -221,7 +221,7 @@ private def mkRecursorInfoAux (cinfo : ConstantInfo) (majorPos? : Option Nat) :
       forallTelescopeReducing motiveType fun motiveTypeParams motiveResultType => do
         checkMotiveResultType declName motiveArgs motiveResultType motiveTypeParams
         let motiveLvl ← getMotiveLevel declName motiveResultType
-        let univLevelPos ← getUnivLevelPos declName cinfo.lparams motiveLvl Ilevels
+        let univLevelPos ← getUnivLevelPos declName cinfo.levelParams motiveLvl Ilevels
         let (produceMotive, recursive) ← getProduceMotiveAndRecursive xs numParams numIndices majorPos motive
         pure {
           recursorName  := declName,

src/Lean/Meta/Tactic/Delta.lean

@@ -12,7 +12,7 @@ namespace Lean.Meta
 def deltaExpand (e : Expr) (p : Name → Bool) : CoreM Expr :=
   Core.transform e fun e =>
     matchConst e.getAppFn (fun _ => return TransformStep.visit e) fun fInfo fLvls => do
-      if p fInfo.name && fInfo.hasValue && fInfo.lparams.length == fLvls.length then
+      if p fInfo.name && fInfo.hasValue && fInfo.levelParams.length == fLvls.length then
         let f := fInfo.instantiateValueLevelParams fLvls
         return TransformStep.visit (f.betaRev e.getAppRevArgs)
       else

src/Lean/Meta/Tactic/Simp/SimpLemmas.lean

@@ -92,7 +92,7 @@ def addSimpLemma (declName : Name) (post : Bool) (attrKind : AttributeKind) (pri
   let cinfo ← getConstInfo declName
   /- The `simp` tactic uses fresh universe metavariables when using a global simp lemma.
      See `SimpLemma.getValue` -/
-  let lemma ← mkSimpLemmaCore (mkConst declName (cinfo.lparams.map mkLevelParam)) (mkConst declName) post prio declName
+  let lemma ← mkSimpLemmaCore (mkConst declName (cinfo.levelParams.map mkLevelParam)) (mkConst declName) post prio declName
   simpExtension.add lemma attrKind
   pure ()
 
@@ -123,10 +123,10 @@ def SimpLemma.getValue (lemma : SimpLemma) : MetaM Expr := do
   match lemma.val with
   | Expr.const declName [] _ =>
     let info ← getConstInfo declName
-    if info.lparams.isEmpty then
+    if info.levelParams.isEmpty then
       return lemma.val
     else
-      return lemma.val.updateConst! (← info.lparams.mapM (fun _ => mkFreshLevelMVar))
+      return lemma.val.updateConst! (← info.levelParams.mapM (fun _ => mkFreshLevelMVar))
   | _ => return lemma.val
 
 end Lean.Meta

src/Lean/Meta/UnificationHint.lean

@@ -110,7 +110,7 @@ where
     traceCtx `Meta.isDefEq.hint <| commitWhen do
       trace[Meta.isDefEq.hint]! "trying hint {candidate} at {t} =?= {s}"
       let cinfo ← getConstInfo candidate
-      let us ← cinfo.lparams.mapM fun _ => mkFreshLevelMVar
+      let us ← cinfo.levelParams.mapM fun _ => mkFreshLevelMVar
       let val := cinfo.instantiateValueLevelParams us
       let (xs, bis, body) ← lambdaMetaTelescope val
       let hint? ← withConfig (fun cfg => { cfg with unificationHints := false }) do

src/Lean/Meta/WHNF.lean

@@ -243,14 +243,14 @@ private def extractIdRhs (e : Expr) : Expr :=
 
 @[specialize] private def deltaDefinition {α} (c : ConstantInfo) (lvls : List Level)
     (failK : Unit → α) (successK : Expr → α) : α :=
-  if c.lparams.length != lvls.length then failK ()
+  if c.levelParams.length != lvls.length then failK ()
   else
     let val := c.instantiateValueLevelParams lvls
     successK (extractIdRhs val)
 
 @[specialize] private def deltaBetaDefinition {α} (c : ConstantInfo) (lvls : List Level) (revArgs : Array Expr)
     (failK : Unit → α) (successK : Expr → α) : α :=
-  if c.lparams.length != lvls.length then
+  if c.levelParams.length != lvls.length then
     failK ()
   else
     let val := c.instantiateValueLevelParams lvls
@@ -418,7 +418,7 @@ mutual
     match e with
     | Expr.app f _ _ =>
       matchConstAux f.getAppFn (fun _ => unfoldProjInst e) fun fInfo fLvls => do
-        if fInfo.lparams.length != fLvls.length then
+        if fInfo.levelParams.length != fLvls.length then
           return none
         else
           let unfoldDefault (_ : Unit) : MetaM (Option Expr) :=