chore: Declaration.lean naming convention

`Declaration.lean` was one of the first Lean 4 files, and was still using an old naming convention. cc @Kha
2021-01-20 15:11:55 -08:00 · 2021-01-20 15:11:55 -08:00 · ea0fda39bc
commit ea0fda39bc
parent d428c388cf
35 changed files with 225 additions and 226 deletions
--- a/src/Lean/Declaration.lean
+++ b/src/Lean/Declaration.lean
@ -60,7 +60,7 @@ end ReducibilityHints
 /-- Base structure for `AxiomVal`, `DefinitionVal`, `TheoremVal`, `InductiveVal`, `ConstructorVal`, `RecursorVal` and `QuotVal`. -/
 structure ConstantVal where
  name : Name
-  lparams : List Name
+  levelParams : List Name
  type : Expr
  deriving Inhabited

@ -68,9 +68,9 @@ structure AxiomVal extends ConstantVal where
  isUnsafe : Bool

@[export lean_mk_axiom_val]
-def mkAxiomValEx (name : Name) (lparams : List Name) (type : Expr) (isUnsafe : Bool) : AxiomVal := {
+def mkAxiomValEx (name : Name) (levelParams : List Name) (type : Expr) (isUnsafe : Bool) : AxiomVal := {
  name := name,
-  lparams := lparams,
+  levelParams := levelParams,
  type := type,
  isUnsafe := isUnsafe
 }
@ -89,9 +89,9 @@ structure DefinitionVal extends ConstantVal where
  deriving Inhabited

@[export lean_mk_definition_val]
-def mkDefinitionValEx (name : Name) (lparams : List Name) (type : Expr) (val : Expr) (hints : ReducibilityHints) (safety : DefinitionSafety) : DefinitionVal := {
+def mkDefinitionValEx (name : Name) (levelParams : List Name) (type : Expr) (val : Expr) (hints : ReducibilityHints) (safety : DefinitionSafety) : DefinitionVal := {
  name := name,
-  lparams := lparams,
+  levelParams := levelParams,
  type := type,
  value := val,
  hints := hints,
@ -110,9 +110,9 @@ structure OpaqueVal extends ConstantVal where
  isUnsafe : Bool

@[export lean_mk_opaque_val]
-def mkOpaqueValEx (name : Name) (lparams : List Name) (type : Expr) (val : Expr) (isUnsafe : Bool) : OpaqueVal := {
+def mkOpaqueValEx (name : Name) (levelParams : List Name) (type : Expr) (val : Expr) (isUnsafe : Bool) : OpaqueVal := {
  name := name,
-  lparams := lparams,
+  levelParams := levelParams,
  type := type,
  value := val,
  isUnsafe := isUnsafe
@ -179,8 +179,8 @@ def Declaration.isUnsafeInductiveDeclEx : Declaration → Bool
    A series of checks are performed by the kernel to check whether a `inductiveDecls`
    is valid or not. -/
 structure InductiveVal extends ConstantVal where
-  nparams : Nat       -- Number of parameters
-  nindices : Nat      -- Number of indices
+  numParams : Nat     -- Number of parameters
+  numIndices : Nat    -- Number of indices
  all : List Name     -- List of all (including this one) inductive datatypes in the mutual declaration containing this one
  ctors : List Name   -- List of all constructors for this inductive datatype
  isRec : Bool        -- `true` Iff it is recursive
@ -190,13 +190,13 @@ structure InductiveVal extends ConstantVal where
  deriving Inhabited

@[export lean_mk_inductive_val]
-def mkInductiveValEx (name : Name) (lparams : List Name) (type : Expr) (nparams nindices : Nat)
+def mkInductiveValEx (name : Name) (levelParams : List Name) (type : Expr) (numParams numIndices : Nat)
    (all ctors : List Name) (isRec isUnsafe isReflexive isNested : Bool) : InductiveVal := {
  name := name
-  lparams := lparams
+  levelParams := levelParams
  type := type
-  nparams := nparams
-  nindices := nindices
+  numParams := numParams
+  numIndices := numIndices
  all := all
  ctors := ctors
  isRec := isRec
@ -213,22 +213,22 @@ def mkInductiveValEx (name : Name) (lparams : List Name) (type : Expr) (nparams
 def InductiveVal.nctors (v : InductiveVal) : Nat := v.ctors.length

 structure ConstructorVal extends ConstantVal where
-  induct  : Name  -- Inductive Type this Constructor is a member of
-  cidx    : Nat   -- Constructor index (i.e., Position in the inductive declaration)
-  nparams : Nat   -- Number of parameters in inductive datatype `induct`
-  nfields : Nat   -- Number of fields (i.e., arity - nparams)
+  induct  : Name    -- Inductive Type this Constructor is a member of
+  cidx    : Nat     -- Constructor index (i.e., Position in the inductive declaration)
+  numParams : Nat   -- Number of parameters in inductive datatype `induct`
+  numFields : Nat   -- Number of fields (i.e., arity - nparams)
  isUnsafe : Bool
  deriving Inhabited

@[export lean_mk_constructor_val]
-def mkConstructorValEx (name : Name) (lparams : List Name) (type : Expr) (induct : Name) (cidx nparams nfields : Nat) (isUnsafe : Bool) : ConstructorVal := {
+def mkConstructorValEx (name : Name) (levelParams : List Name) (type : Expr) (induct : Name) (cidx numParams numFields : Nat) (isUnsafe : Bool) : ConstructorVal := {
  name := name,
-  lparams := lparams,
+  levelParams := levelParams,
  type := type,
  induct := induct,
  cidx := cidx,
-  nparams := nparams,
-  nfields := nfields,
+  numParams := numParams,
+  numFields := numFields,
  isUnsafe := isUnsafe
 }

@ -241,33 +241,33 @@ structure RecursorRule where
  rhs : Expr    -- Right hand side of the reduction rule

 structure RecursorVal extends ConstantVal where
-  all : List Name            -- List of all inductive datatypes in the mutual declaration that generated this recursor
-  nparams : Nat              -- Number of parameters
-  nindices : Nat             -- Number of indices
-  nmotives : Nat             -- Number of motives
-  nminors : Nat              -- Number of minor premises
-  rules : List RecursorRule  -- A reduction for each Constructor
-  k : Bool                   -- It supports K-like reduction
+  all : List Name              -- List of all inductive datatypes in the mutual declaration that generated this recursor
+  numParams : Nat              -- Number of parameters
+  numIndices : Nat             -- Number of indices
+  numMotives : Nat             -- Number of motives
+  numMinors : Nat              -- Number of minor premises
+  rules : List RecursorRule    -- A reduction for each Constructor
+  k : Bool                     -- It supports K-like reduction
  isUnsafe : Bool

@[export lean_mk_recursor_val]
-def mkRecursorValEx (name : Name) (lparams : List Name) (type : Expr) (all : List Name) (nparams nindices nmotives nminors : Nat)
+def mkRecursorValEx (name : Name) (levelParams : List Name) (type : Expr) (all : List Name) (numParams numIndices numMotives numMinors : Nat)
    (rules : List RecursorRule) (k isUnsafe : Bool) : RecursorVal := {
-  name := name, lparams := lparams, type := type, all := all, nparams := nparams, nindices := nindices,
-  nmotives := nmotives, nminors := nminors, rules := rules, k := k, isUnsafe := isUnsafe
+  name := name, levelParams := levelParams, type := type, all := all, numParams := numParams, numIndices := numIndices,
+  numMotives := numMotives, numMinors := numMinors, rules := rules, k := k, isUnsafe := isUnsafe
 }

@[export lean_recursor_k] def RecursorVal.kEx (v : RecursorVal) : Bool := v.k
@[export lean_recursor_is_unsafe] def RecursorVal.isUnsafeEx (v : RecursorVal) : Bool := v.isUnsafe

 def RecursorVal.getMajorIdx (v : RecursorVal) : Nat :=
-  v.nparams + v.nmotives + v.nminors + v.nindices
+  v.numParams + v.numMotives + v.numMinors + v.numIndices

 def RecursorVal.getFirstIndexIdx (v : RecursorVal) : Nat :=
-  v.nparams + v.nmotives + v.nminors
+  v.numParams + v.numMotives + v.numMinors

 def RecursorVal.getFirstMinorIdx (v : RecursorVal) : Nat :=
-  v.nparams + v.nmotives
+  v.numParams + v.numMotives

 def RecursorVal.getInduct (v : RecursorVal) : Name :=
  v.name.getPrefix
@ -282,8 +282,8 @@ structure QuotVal extends ConstantVal where
  kind : QuotKind

@[export lean_mk_quot_val]
-def mkQuotValEx (name : Name) (lparams : List Name) (type : Expr) (kind : QuotKind) : QuotVal := {
-  name := name, lparams := lparams, type := type, kind := kind
+def mkQuotValEx (name : Name) (levelParams : List Name) (type : Expr) (kind : QuotKind) : QuotVal := {
+  name := name, levelParams := levelParams, type := type, kind := kind
 }

@[export lean_quot_val_kind] def QuotVal.kindEx (v : QuotVal) : QuotKind := v.kind
@ -325,7 +325,7 @@ def name (d : ConstantInfo) : Name :=
  d.toConstantVal.name

 def lparams (d : ConstantInfo) : List Name :=
-  d.toConstantVal.lparams
+  d.toConstantVal.levelParams

 def type (d : ConstantInfo) : Expr :=
  d.toConstantVal.type
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@ -65,7 +65,7 @@ def declareTacticSyntax (tactic : Syntax) : TermElabM Name :=
    let val ← elabTerm tactic type
    let val ← instantiateMVars val
    trace[Elab.autoParam]! val
-    let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque,
+    let decl := Declaration.defnDecl { name := name, levelParams := [], type := type, value := val, hints := ReducibilityHints.opaque,
                                       safety := DefinitionSafety.safe }
    addDecl decl
    compileDecl decl
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@ -93,7 +93,7 @@ private def elabTParserMacroAux (prec : Syntax) (e : Syntax) : TermElabM Syntax
 private def mkNativeReflAuxDecl (type val : Expr) : TermElabM Name := do
  let auxName ← mkAuxName `_nativeRefl
  let decl := Declaration.defnDecl {
-    name := auxName, lparams := [], type := type, value := val,
+    name := auxName, levelParams := [], type := type, value := val,
    hints := ReducibilityHints.abbrev,
    safety := DefinitionSafety.safe
  }
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@ -598,7 +598,7 @@ unsafe def elabEvalUnsafe : CommandElab
    let addAndCompile (value : Expr) : TermElabM Unit := do
      let type ← inferType value
      let decl := Declaration.defnDecl {
-        name := n, lparams := [], type := type,
+        name := n, levelParams := [], type := type,
        value := value, hints := ReducibilityHints.opaque,
        safety := DefinitionSafety.unsafe
      }
--- a/src/Lean/Elab/Declaration.lean
+++ b/src/Lean/Elab/Declaration.lean
@ -74,10 +74,10 @@ def elabAxiom (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit := do
    | Except.error msg      => throwErrorAt stx msg
    | Except.ok levelParams =>
      let decl := Declaration.axiomDecl {
-        name     := declName,
-        lparams  := levelParams,
-        type     := type,
-        isUnsafe := modifiers.isUnsafe
+        name        := declName,
+        levelParams := levelParams,
+        type        := type,
+        isUnsafe    := modifiers.isUnsafe
      }
      Term.ensureNoUnassignedMVars decl
      addDecl decl
--- a/src/Lean/Elab/Deriving/BEq.lean
+++ b/src/Lean/Elab/Deriving/BEq.lean
@ -22,7 +22,7 @@ where
  mkElseAlt : TermElabM Syntax := do
    let mut patterns := #[]
    -- add `_` pattern for indices
-    for i in [:indVal.nindices] do
+    for i in [:indVal.numIndices] do
      patterns := patterns.push (← `(_))
    patterns := patterns.push (← `(_))
    patterns := patterns.push (← `(_))
@ -37,17 +37,17 @@ where
        let type ← Core.betaReduce type -- we 'beta-reduce' to eliminate "artificial" dependencies
        let mut patterns := #[]
        -- add `_` pattern for indices
-        for i in [:indVal.nindices] do
+        for i in [:indVal.numIndices] do
          patterns := patterns.push (← `(_))
        let mut ctorArgs1 := #[]
        let mut ctorArgs2 := #[]
        let mut rhs ← `(true)
        -- add `_` for inductive parameters, they are inaccessible
-        for i in [:indVal.nparams] do
+        for i in [:indVal.numParams] do
          ctorArgs1 := ctorArgs1.push (← `(_))
          ctorArgs2 := ctorArgs2.push (← `(_))
-        for i in [:ctorInfo.nfields] do
-          let x := xs[indVal.nparams + i]
+        for i in [:ctorInfo.numFields] do
+          let x := xs[indVal.numParams + i]
          if type.containsFVar x.fvarId! then
            -- If resulting type depends on this field, we don't need to compare
            ctorArgs1 := ctorArgs1.push (← `(_))
--- a/src/Lean/Elab/Deriving/DecEq.lean
+++ b/src/Lean/Elab/Deriving/DecEq.lean
@ -41,7 +41,7 @@ where
      for ctorName₂ in indVal.ctors do
        let mut patterns := #[]
        -- add `_` pattern for indices
-        for i in [:indVal.nindices] do
+        for i in [:indVal.numIndices] do
          patterns := patterns.push (← `(_))
        if ctorName₁ == ctorName₂ then
          let alt ← forallTelescopeReducing ctorInfo.type fun xs type => do
@ -50,12 +50,12 @@ where
            let mut ctorArgs1 := #[]
            let mut ctorArgs2 := #[]
            -- add `_` for inductive parameters, they are inaccessible
-            for i in [:indVal.nparams] do
+            for i in [:indVal.numParams] do
              ctorArgs1 := ctorArgs1.push (← `(_))
              ctorArgs2 := ctorArgs2.push (← `(_))
            let mut todo := #[]
-            for i in [:ctorInfo.nfields] do
-              let x := xs[indVal.nparams + i]
+            for i in [:ctorInfo.numFields] do
+              let x := xs[indVal.numParams + i]
              if type.containsFVar x.fvarId! then
                -- If resulting type depends on this field, we don't need to compare
                ctorArgs1 := ctorArgs1.push (← `(_))
--- a/src/Lean/Elab/Deriving/Inhabited.lean
+++ b/src/Lean/Elab/Deriving/Inhabited.lean
@ -63,7 +63,7 @@ where
    let ctorVal ← getConstInfoCtor ctorName
    let mut indArgs := #[]
    let mut binders := #[]
-    for i in [:indVal.nparams + indVal.nindices] do
+    for i in [:indVal.numParams + indVal.numIndices] do
      let arg := mkIdent (← mkFreshUserName `a)
      indArgs := indArgs.push arg
      let binder ← `(implicitBinderF| { $arg:ident })
@ -73,9 +73,9 @@ where
        binders := binders.push binder
    let type ← `(Inhabited (@$(mkIdent inductiveTypeName):ident $indArgs:ident*))
    let mut ctorArgs := #[]
-    for i in [:ctorVal.nparams] do
+    for i in [:ctorVal.numParams] do
      ctorArgs := ctorArgs.push (← `(_))
-    for i in [:ctorVal.nfields] do
+    for i in [:ctorVal.numFields] do
      ctorArgs := ctorArgs.push (← `(arbitrary))
    let val ← `(⟨@$(mkIdent ctorName):ident $ctorArgs:ident*⟩)
    `(instance $binders:explicitBinder* : $type := $val)
@ -83,10 +83,10 @@ where
  mkInstanceCmd? : TermElabM (Option Syntax) := do
    let ctorVal ← getConstInfoCtor ctorName
    forallTelescopeReducing ctorVal.type fun xs _ =>
-      addLocalInstancesForParams xs[:ctorVal.nparams] fun localInst2Index => do
+      addLocalInstancesForParams xs[:ctorVal.numParams] fun localInst2Index => do
        let mut usedInstIdxs := {}
        let mut ok := true
-        for i in [ctorVal.nparams:xs.size] do
+        for i in [ctorVal.numParams:xs.size] do
          let x := xs[i]
          let instType ← mkAppM `Inhabited #[(← inferType x)]
          trace[Elab.Deriving.inhabited]! "checking {instType} for '{ctorName}'"
--- a/src/Lean/Elab/Deriving/Repr.lean
+++ b/src/Lean/Elab/Deriving/Repr.lean
@ -23,7 +23,7 @@ def mkReprHeader (ctx : Context) (indVal : InductiveVal) : TermElabM Header := d
 def mkBodyForStruct (ctx : Context) (header : Header) (indVal : InductiveVal) : TermElabM Syntax := do
  let ctorVal ← getConstInfoCtor indVal.ctors.head!
  let fieldNames ← getStructureFields (← getEnv) indVal.name
-  let numParams := indVal.nparams
+  let numParams := indVal.numParams
  let target    := mkIdent header.targetNames[0]
  forallTelescopeReducing ctorVal.type fun xs _ => do
    let mut fields : Syntax ← `(Format.nil)
@ -56,16 +56,16 @@ where
      let alt ← forallTelescopeReducing ctorInfo.type fun xs type => do
        let mut patterns := #[]
        -- add `_` pattern for indices
-        for i in [:indVal.nindices] do
+        for i in [:indVal.numIndices] do
          patterns := patterns.push (← `(_))
        let mut ctorArgs := #[]
        let mut rhs := Syntax.mkStrLit (toString ctorInfo.name)
        let mut rhs ← `(Format.text $rhs)
        -- add `_` for inductive parameters, they are inaccessible
-        for i in [:indVal.nparams] do
+        for i in [:indVal.numParams] do
          ctorArgs := ctorArgs.push (← `(_))
-        for i in [:ctorInfo.nfields] do
-          let x := xs[indVal.nparams + i]
+        for i in [:ctorInfo.numFields] do
+          let x := xs[indVal.numParams + i]
          let a := mkIdent (← mkFreshUserName `a)
          ctorArgs := ctorArgs.push a
          if (← inferType x).isAppOf indVal.name then
--- a/src/Lean/Elab/Deriving/Util.lean
+++ b/src/Lean/Elab/Deriving/Util.lean
@ -32,7 +32,7 @@ def mkImplicitBinders (argNames : Array Name) : TermElabM (Array Syntax) :=
    `(implicitBinderF| { $(mkIdent argName) })

 def mkInstImplicitBinders (className : Name) (indVal : InductiveVal) (argNames : Array Name) : TermElabM (Array Syntax) :=
-  forallBoundedTelescope indVal.type indVal.nparams fun xs _ => do
+  forallBoundedTelescope indVal.type indVal.numParams fun xs _ => do
    let mut binders := #[]
    for i in [:xs.size] do
      try
@ -75,7 +75,7 @@ def mkLocalInstanceLetDecls (ctx : Context) (className : Name) (argNames : Array
    let indVal       := ctx.typeInfos[i]
    let auxFunName   := ctx.auxFunNames[i]
    let currArgNames ← mkInductArgNames indVal
-    let numParams    := indVal.nparams
+    let numParams    := indVal.numParams
    let currIndices  := currArgNames[numParams:]
    let binders      ← mkImplicitBinders currIndices
    let argNamesNew  := argNames[:numParams] ++ currIndices
@ -134,7 +134,7 @@ def mkHeader (ctx : Context) (className : Name) (arity : Nat) (indVal : Inductiv
 def mkDiscrs (header : Header) (indVal : InductiveVal) : TermElabM (Array Syntax) := do
  let mut discrs := #[]
  -- add indices
-  for argName in header.argNames[indVal.nparams:] do
+  for argName in header.argNames[indVal.numParams:] do
    discrs := discrs.push (← mkDiscr argName)
  return discrs ++ (← header.targetNames.mapM mkDiscr)

--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@ -202,7 +202,7 @@ private def throwCtorExpected {α} : M α :=
  throwError "invalid pattern, constructor or constant marked with '[matchPattern]' expected"

 private def getNumExplicitCtorParams (ctorVal : ConstructorVal) : TermElabM Nat :=
-  forallBoundedTelescope ctorVal.type ctorVal.nparams fun ps _ => do
+  forallBoundedTelescope ctorVal.type ctorVal.numParams fun ps _ => do
    let mut result := 0
    for p in ps do
      let localDecl ← getLocalDecl p.fvarId!
@ -250,7 +250,7 @@ private def finalize (ctx : Context) : M Syntax := do
 private def isNextArgAccessible (ctx : Context) : Bool :=
  let i := ctx.paramDeclIdx
  match ctx.ctorVal? with
-  | some ctorVal => i ≥ ctorVal.nparams -- For constructor applications only fields are accessible
+  | some ctorVal => i ≥ ctorVal.numParams -- For constructor applications only fields are accessible
  | none =>
    if h : i < ctx.paramDecls.size then
      -- For `[matchPattern]` applications, only explicit parameters are accessible.
@ -649,10 +649,10 @@ partial def main (e : Expr) : M Pattern := do
      main newE
    else matchConstCtor e.getAppFn (fun _ => throwInvalidPattern e) fun v us => do
      let args := e.getAppArgs
-      unless args.size == v.nparams + v.nfields do
+      unless args.size == v.numParams + v.numFields do
        throwInvalidPattern e
-      let params := args.extract 0 v.nparams
-      let fields := args.extract v.nparams args.size
+      let params := args.extract 0 v.numParams
+      let fields := args.extract v.numParams args.size
      let fields ← fields.mapM main
      pure $ Pattern.ctor v.name us params.toList fields.toList

@ -916,8 +916,8 @@ where
      elabMatchCore stx expectedType?

@[builtinInit] private def regTraceClasses : IO Unit := do
-registerTraceClass `Elab.match;
-pure ()
+  registerTraceClass `Elab.match;
+  pure ()

 -- parser!:leadPrec "nomatch " >> termParser
@[builtinTermElab «nomatch»] def elabNoMatch : TermElab := fun stx expectedType? =>
@ -928,6 +928,4 @@ pure ()
      elabMatchAux #[discr] #[] mkNullNode expectedType
  | _ => throwUnsupportedSyntax

-end Term
-end Elab
-end Lean
+end Lean.Elab.Term
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@ -527,13 +527,13 @@ def pushMain (preDefs : Array PreDefinition) (sectionVars : Array Expr) (mainHea
    let val  ← mkLambdaFVars sectionVars mainVals[i]
    let type ← mkForallFVars sectionVars header.type
    return preDefs.push {
-      ref       := getDeclarationSelectionRef header.ref
-      kind      := header.kind
-      declName  := header.declName
-      lparams   := [], -- we set it later
-      modifiers := header.modifiers
-      type      := type
-      value     := val
+      ref         := getDeclarationSelectionRef header.ref
+      kind        := header.kind
+      declName    := header.declName
+      levelParams := [], -- we set it later
+      modifiers   := header.modifiers
+      type        := type
+      value       := val
    }

 def pushLetRecs (preDefs : Array PreDefinition) (letRecClosures : List LetRecClosure) (kind : DefKind) (modifiers : Modifiers) : Array PreDefinition :=
@ -541,13 +541,13 @@ def pushLetRecs (preDefs : Array PreDefinition) (letRecClosures : List LetRecClo
    let type := Closure.mkForall c.localDecls c.toLift.type
    let val  := Closure.mkLambda c.localDecls c.toLift.val
    preDefs.push {
-      ref       := c.ref
-      kind      := kind
-      declName  := c.toLift.declName
-      lparams   := [] -- we set it later
-      modifiers := { modifiers with attrs := c.toLift.attrs }
-      type      := type
-      value     := val
+      ref         := c.ref
+      kind        := kind
+      declName    := c.toLift.declName
+      levelParams := [] -- we set it later
+      modifiers   := { modifiers with attrs := c.toLift.attrs }
+      type        := type
+      value       := val
    }

 def getKindForLetRecs (mainHeaders : Array DefViewElabHeader) : DefKind :=
--- a/src/Lean/Elab/PreDefinition/Basic.lean
+++ b/src/Lean/Elab/PreDefinition/Basic.lean
@ -18,13 +18,13 @@ A (potentially recursive) definition.
 The elaborator converts it into Kernel definitions using many different strategies.
 -/
 structure PreDefinition where
-  ref       : Syntax
-  kind      : DefKind
-  lparams   : List Name
-  modifiers : Modifiers
-  declName  : Name
-  type      : Expr
-  value     : Expr
+  ref         : Syntax
+  kind        : DefKind
+  levelParams : List Name
+  modifiers   : Modifiers
+  declName    : Name
+  type        : Expr
+  value       : Expr
  deriving Inhabited

 def instantiateMVarsAtPreDecls (preDefs : Array PreDefinition) : TermElabM (Array PreDefinition) :=
@ -61,17 +61,17 @@ private def shareCommon (preDefs : Array PreDefinition) : Array PreDefinition :=

 def fixLevelParams (preDefs : Array PreDefinition) (scopeLevelNames allUserLevelNames : List Name) : TermElabM (Array PreDefinition) := do
  let preDefs := shareCommon preDefs
-  let lparams ← getLevelParamsPreDecls preDefs scopeLevelNames allUserLevelNames
-  let us := lparams.map mkLevelParam
+  let levelParams ← getLevelParamsPreDecls preDefs scopeLevelNames allUserLevelNames
+  let us := levelParams.map mkLevelParam
  let fixExpr (e : Expr) : Expr :=
    e.replace fun c => match c with
      | Expr.const declName _ _ => if preDefs.any fun preDef => preDef.declName == declName then some $ Lean.mkConst declName us else none
      | _ => none
  pure $ preDefs.map fun preDef =>
    { preDef with
-      type    := fixExpr preDef.type,
-      value   := fixExpr preDef.value,
-      lparams := lparams }
+      type        := fixExpr preDef.type,
+      value       := fixExpr preDef.value,
+      levelParams := levelParams }

 def applyAttributesOf (preDefs : Array PreDefinition) (applicationTime : AttributeApplicationTime) : TermElabM Unit := do
  for preDef in preDefs do
@ -87,7 +87,7 @@ def abstractNestedProofs (preDef : PreDefinition) : MetaM PreDefinition :=
 /- Auxiliary method for (temporarily) adding pre definition as an axiom -/
 def addAsAxiom (preDef : PreDefinition) : MetaM Unit := do
  withRef preDef.ref do
-    addDecl <| Declaration.axiomDecl { name := preDef.declName, lparams := preDef.lparams, type := preDef.type, isUnsafe := preDef.modifiers.isUnsafe }
+    addDecl <| Declaration.axiomDecl { name := preDef.declName, levelParams := preDef.levelParams, type := preDef.type, isUnsafe := preDef.modifiers.isUnsafe }

 private def shouldGenCodeFor (preDef : PreDefinition) : Bool :=
  !preDef.kind.isTheorem && !preDef.modifiers.isNoncomputable
@ -100,16 +100,16 @@ private def addNonRecAux (preDef : PreDefinition) (compile : Bool) : TermElabM U
      match preDef.kind with
      | DefKind.«example» => unreachable!
      | DefKind.«theorem» =>
-        Declaration.thmDecl { name := preDef.declName, lparams := preDef.lparams, type := preDef.type, value := preDef.value }
+        Declaration.thmDecl { name := preDef.declName, levelParams := preDef.levelParams, type := preDef.type, value := preDef.value }
      | DefKind.«opaque»  =>
-        Declaration.opaqueDecl { name := preDef.declName, lparams := preDef.lparams, type := preDef.type, value := preDef.value,
+        Declaration.opaqueDecl { name := preDef.declName, levelParams := preDef.levelParams, type := preDef.type, value := preDef.value,
                                 isUnsafe := preDef.modifiers.isUnsafe }
      | DefKind.«abbrev»  =>
-        Declaration.defnDecl { name := preDef.declName, lparams := preDef.lparams, type := preDef.type, value := preDef.value,
+        Declaration.defnDecl { name := preDef.declName, levelParams := preDef.levelParams, type := preDef.type, value := preDef.value,
                               hints := ReducibilityHints.«abbrev»,
                               safety := if preDef.modifiers.isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe }
      | DefKind.«def»  =>
-        Declaration.defnDecl { name := preDef.declName, lparams := preDef.lparams, type := preDef.type, value := preDef.value,
+        Declaration.defnDecl { name := preDef.declName, levelParams := preDef.levelParams, type := preDef.type, value := preDef.value,
                               hints := ReducibilityHints.regular (getMaxHeight env preDef.value + 1),
                               safety := if preDef.modifiers.isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe }
    addDecl decl
@ -127,12 +127,12 @@ def addNonRec (preDef : PreDefinition) : TermElabM Unit := do
 def addAndCompileUnsafe (preDefs : Array PreDefinition) (safety := DefinitionSafety.unsafe) : TermElabM Unit :=
  withRef preDefs[0].ref do
    let decl := Declaration.mutualDefnDecl $ preDefs.toList.map fun preDef => {
-        name     := preDef.declName,
-        lparams  := preDef.lparams,
-        type     := preDef.type,
-        value    := preDef.value,
-        safety   := safety,
-        hints    := ReducibilityHints.opaque
+        name        := preDef.declName
+        levelParams := preDef.levelParams
+        type        := preDef.type
+        value       := preDef.value
+        safety      := safety
+        hints       := ReducibilityHints.opaque
      }
    addDecl decl
    applyAttributesOf preDefs AttributeApplicationTime.afterTypeChecking
--- a/src/Lean/Elab/PreDefinition/Structural.lean
+++ b/src/Lean/Elab/PreDefinition/Structural.lean
@ -119,8 +119,8 @@ private partial def findRecArg {α} (numFixed : Nat) (xs : Array Expr) (k : RecA
          loop (i+1)
        else
          let indArgs    := xType.getAppArgs
-          let indParams  := indArgs.extract 0 indInfo.nparams
-          let indIndices := indArgs.extract indInfo.nparams indArgs.size
+          let indParams  := indArgs.extract 0 indInfo.numParams
+          let indIndices := indArgs.extract indInfo.numParams indArgs.size
          if !indIndices.all Expr.isFVar then
            orelse'
              (throwError! "argument #{i+1} was not used because its type is an inductive family and indices are not variables{indentExpr xType}")
--- a/src/Lean/Elab/Print.lean
+++ b/src/Lean/Elab/Print.lean
@ -11,8 +11,8 @@ namespace Lean.Elab.Command
 private def throwUnknownId (id : Name) : CommandElabM Unit :=
  throwError! "unknown identifier '{mkConst id}'"

-private def lparamsToMessageData (lparams : List Name) : MessageData :=
-  match lparams with
+private def levelParamsToMessageData (levelParams : List Name) : MessageData :=
+  match levelParams with
  | []    => ""
  | u::us => do
    let mut m := m!".\{{u}"
@ -20,7 +20,7 @@ private def lparamsToMessageData (lparams : List Name) : MessageData :=
      m := m ++ ", " ++ u
    return m ++ "}"

-private def mkHeader (kind : String) (id : Name) (lparams : List Name) (type : Expr) (safety : DefinitionSafety) : CommandElabM MessageData := do
+private def mkHeader (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (safety : DefinitionSafety) : CommandElabM MessageData := do
  let m : MessageData :=
    match safety with
    | DefinitionSafety.unsafe  => "unsafe "
@ -30,26 +30,26 @@ private def mkHeader (kind : String) (id : Name) (lparams : List Name) (type : E
  let (m, id) := match privateToUserName? id with
    | some id => (m ++ "private ", id)
    | none    => (m, id)
-  let m := m ++ kind ++ " " ++ id ++ lparamsToMessageData lparams ++ " : " ++ type
+  let m := m ++ kind ++ " " ++ id ++ levelParamsToMessageData levelParams ++ " : " ++ type
  pure m

-private def mkHeader' (kind : String) (id : Name) (lparams : List Name) (type : Expr) (isUnsafe : Bool) : CommandElabM MessageData :=
-  mkHeader kind id lparams type (if isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe)
+private def mkHeader' (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (isUnsafe : Bool) : CommandElabM MessageData :=
+  mkHeader kind id levelParams type (if isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe)

-private def printDefLike (kind : String) (id : Name) (lparams : List Name) (type : Expr) (value : Expr) (safety := DefinitionSafety.safe) : CommandElabM Unit := do
-  let m ← mkHeader kind id lparams type safety
+private def printDefLike (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (value : Expr) (safety := DefinitionSafety.safe) : CommandElabM Unit := do
+  let m ← mkHeader kind id levelParams type safety
  let m := m ++ " :=" ++ Format.line ++ value
  logInfo m

-private def printAxiomLike (kind : String) (id : Name) (lparams : List Name) (type : Expr) (isUnsafe := false) : CommandElabM Unit := do
-  logInfo (← mkHeader' kind id lparams type isUnsafe)
+private def printAxiomLike (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (isUnsafe := false) : CommandElabM Unit := do
+  logInfo (← mkHeader' kind id levelParams type isUnsafe)

-private def printQuot (kind : QuotKind) (id : Name) (lparams : List Name) (type : Expr) : CommandElabM Unit := do
-  printAxiomLike "Quotient primitive" id lparams type
+private def printQuot (kind : QuotKind) (id : Name) (levelParams : List Name) (type : Expr) : CommandElabM Unit := do
+  printAxiomLike "Quotient primitive" id levelParams type

-private def printInduct (id : Name) (lparams : List Name) (nparams : Nat) (nindices : Nat) (type : Expr)
+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 lparams type isUnsafe
+  let mut m ← mkHeader' "inductive" id levelParams type isUnsafe
  m := m ++ Format.line ++ "constructors:"
  for ctor in ctors do
    let cinfo ← getConstInfo ctor
@ -58,15 +58,15 @@ private def printInduct (id : Name) (lparams : List Name) (nparams : Nat) (nindi

 private def printIdCore (id : Name) : CommandElabM Unit := do
  match (← getEnv).find? id with
-  | ConstantInfo.axiomInfo { lparams := us, type := t, isUnsafe := u, .. } => printAxiomLike "axiom" id us t u
-  | ConstantInfo.defnInfo  { lparams := us, type := t, value := v, safety := s, .. } => printDefLike "def" id us t v s
-  | ConstantInfo.thmInfo  { lparams := us, type := t, value := v, .. } => printDefLike "theorem" id us t v
-  | ConstantInfo.opaqueInfo  { lparams := us, type := t, isUnsafe := u, .. } => printAxiomLike "constant" id us t u
-  | ConstantInfo.quotInfo  { kind := kind, lparams := us, type := t, .. } => printQuot kind id us t
-  | ConstantInfo.ctorInfo { lparams := us, type := t, isUnsafe := u, .. } => printAxiomLike "constructor" id us t u
-  | ConstantInfo.recInfo { lparams := us, type := t, isUnsafe := u, .. } => printAxiomLike "recursor" id us t u
-  | ConstantInfo.inductInfo { lparams := us, nparams := nparams, nindices := nindices, type := t, ctors := ctors, isUnsafe := u, .. } =>
-    printInduct id us nparams nindices t ctors u
+  | ConstantInfo.axiomInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "axiom" id us t u
+  | ConstantInfo.defnInfo  { levelParams := us, type := t, value := v, safety := s, .. } => printDefLike "def" id us t v s
+  | ConstantInfo.thmInfo  { levelParams := us, type := t, value := v, .. } => printDefLike "theorem" id us t v
+  | ConstantInfo.opaqueInfo  { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "constant" id us t u
+  | ConstantInfo.quotInfo  { kind := kind, levelParams := us, type := t, .. } => printQuot kind id us t
+  | ConstantInfo.ctorInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "constructor" id us t u
+  | ConstantInfo.recInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "recursor" id us t u
+  | ConstantInfo.inductInfo { levelParams := us, numParams := numParams, numIndices := numIndices, type := t, ctors := ctors, isUnsafe := u, .. } =>
+    printInduct id us numParams numIndices t ctors u
  | none => throwUnknownId id

 private def printId (id : Name) : CommandElabM Unit := do
--- a/src/Lean/Elab/StructInst.lean
+++ b/src/Lean/Elab/StructInst.lean
@ -514,11 +514,11 @@ private def propagateExpectedType (type : Expr) (numFields : Nat) (expectedType?
          discard <| isDefEq expectedType typeBody

 private def mkCtorHeader (ctorVal : ConstructorVal) (expectedType? : Option Expr) : TermElabM CtorHeaderResult := do
-  let lvls ← ctorVal.lparams.mapM fun _ => mkFreshLevelMVar
-  let val  := Lean.mkConst ctorVal.name lvls
-  let type := (ConstantInfo.ctorInfo ctorVal).instantiateTypeLevelParams lvls
-  let r ← mkCtorHeaderAux ctorVal.nparams type val #[]
-  propagateExpectedType r.ctorFnType ctorVal.nfields expectedType?
+  let us ← ctorVal.levelParams.mapM fun _ => mkFreshLevelMVar
+  let val  := Lean.mkConst ctorVal.name us
+  let type := (ConstantInfo.ctorInfo ctorVal).instantiateTypeLevelParams us
+  let r ← mkCtorHeaderAux ctorVal.numParams type val #[]
+  propagateExpectedType r.ctorFnType ctorVal.numFields expectedType?
  synthesizeAppInstMVars r.instMVars
  pure r

--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@ -1436,7 +1436,7 @@ unsafe def evalExpr (α) (typeName : Name) (value : Expr) : TermElabM α :=
    unless type.isConstOf typeName do
      throwError! "unexpected type at evalExpr{indentExpr type}"
    let decl := Declaration.defnDecl {
-       name := name, lparams := [], type := type,
+       name := name, levelParams := [], type := type,
       value := value, hints := ReducibilityHints.opaque,
       safety := DefinitionSafety.unsafe
    }
--- a/src/Lean/KeyedDeclsAttribute.lean
+++ b/src/Lean/KeyedDeclsAttribute.lean
@ -102,7 +102,7 @@ def declareBuiltin {γ} (df : Def γ) (attrDeclName : Name) (env : Environment)
  let name := `_regBuiltin ++ declName
  let type := mkApp (mkConst `IO) (mkConst `Unit)
  let val  := mkAppN (mkConst `Lean.KeyedDeclsAttribute.addBuiltin) #[mkConst df.valueTypeName, mkConst attrDeclName, toExpr key, mkConst declName]
-  let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque,
+  let decl := Declaration.defnDecl { name := name, levelParams := [], type := type, value := val, hints := ReducibilityHints.opaque,
                                     safety := DefinitionSafety.safe }
  match env.addAndCompile {} decl with
  -- TODO: pretty print error
--- a/src/Lean/Meta/Closure.lean
+++ b/src/Lean/Meta/Closure.lean
@ -351,12 +351,12 @@ def mkAuxDefinition (name : Name) (type : Expr) (value : Expr) (zeta : Bool := f
  let result ← Closure.mkValueTypeClosure type value zeta
  let env ← getEnv
  let decl := Declaration.defnDecl {
-    name     := name,
-    lparams  := result.levelParams.toList,
-    type     := result.type,
-    value    := result.value,
-    hints    := ReducibilityHints.regular (getMaxHeight env result.value + 1),
-    safety   := if env.hasUnsafe result.type || env.hasUnsafe result.value then DefinitionSafety.unsafe else DefinitionSafety.safe
+    name        := name,
+    levelParams := result.levelParams.toList,
+    type        := result.type,
+    value       := result.value,
+    hints       := ReducibilityHints.regular (getMaxHeight env result.value + 1),
+    safety      := if env.hasUnsafe result.type || env.hasUnsafe result.value then DefinitionSafety.unsafe else DefinitionSafety.safe
  }
  trace[Meta.debug]! "{name} : {result.type} := {result.value}"
  addDecl decl
--- a/src/Lean/Meta/InferType.lean
+++ b/src/Lean/Meta/InferType.lean
@ -99,7 +99,7 @@ private def inferProjType (structName : Name) (idx : Nat) (e : Expr) : MetaM Exp
  let structType ← inferType e
  let structType ← whnf structType
  matchConstStruct structType.getAppFn failed fun structVal structLvls ctorVal =>
-    let n := structVal.nparams
+    let n := structVal.numParams
    let structParams := structType.getAppArgs
    if n != structParams.size then failed ()
    else do
--- a/src/Lean/Meta/Match/Match.lean
+++ b/src/Lean/Meta/Match/Match.lean
@ -299,7 +299,7 @@ def processInaccessibleAsCtor (alt : Alt) (ctorName : Name) : MetaM (Option Alt)
      match e.constructorApp? env with
      | some (ctorVal, ctorArgs) =>
        if ctorVal.name == ctorName then
-          let fields := ctorArgs.extract ctorVal.nparams ctorArgs.size
+          let fields := ctorArgs.extract ctorVal.numParams ctorArgs.size
          let fields := fields.toList.map Pattern.inaccessible
          pure $ some { alt with patterns := fields ++ ps }
        else
@ -370,7 +370,7 @@ private def processNonVariable (p : Problem) : MetaM Problem :=
        | Pattern.inaccessible _ :: _ => processInaccessibleAsCtor alt ctorVal.name
        | p :: _  => throwError! "failed to compile pattern matching, inaccessible pattern or constructor expected{indentD p.toMessageData}"
        | _       => unreachable!
-      let xFields := xArgs.extract ctorVal.nparams xArgs.size
+      let xFields := xArgs.extract ctorVal.numParams xArgs.size
      pure { p with alts := alts, vars := xFields.toList ++ xs }
    | none =>
      let alts ← p.alts.filterMapM fun alt => match alt.patterns with
--- a/src/Lean/Meta/RecursorInfo.lean
+++ b/src/Lean/Meta/RecursorInfo.lean
@ -68,13 +68,13 @@ end RecursorInfo

 private def mkRecursorInfoForKernelRec (declName : Name) (val : RecursorVal) : MetaM RecursorInfo := do
  let ival ← getConstInfoInduct val.getInduct
-  let numLParams    := ival.lparams.length
+  let numLParams    := ival.levelParams.length
  let univLevelPos  := (List.range numLParams).map RecursorUnivLevelPos.majorType
-  let univLevelPos  := if val.lparams.length == numLParams then univLevelPos else RecursorUnivLevelPos.motive :: univLevelPos
-  let produceMotive := List.replicate val.nminors true
-  let paramsPos     := (List.range val.nparams).map some
-  let indicesPos    := (List.range val.nindices).map fun pos => val.nparams + pos
-  let numArgs       := val.nindices + val.nparams + val.nminors + val.nmotives + 1
+  let univLevelPos  := if val.levelParams.length == numLParams then univLevelPos else RecursorUnivLevelPos.motive :: univLevelPos
+  let produceMotive := List.replicate val.numMinors true
+  let paramsPos     := (List.range val.numParams).map some
+  let indicesPos    := (List.range val.numIndices).map fun pos => val.numParams + pos
+  let numArgs       := val.numIndices + val.numParams + val.numMinors + val.numMotives + 1
  pure {
    recursorName  := declName,
    typeName      := val.getInduct,
@ -100,7 +100,7 @@ private def getMajorPosIfAuxRecursor? (declName : Name) (majorPos? : Option Nat)
        pure none
      else do
        let val ← getConstInfoRec (mkRecName p)
-        pure $ some (val.nparams + val.nindices + (if s == casesOnSuffix then 1 else val.nmotives))
+        pure $ some (val.numParams + val.numIndices + (if s == casesOnSuffix then 1 else val.numMotives))
    | _ => pure none

 private def checkMotive (declName : Name) (motive : Expr) (motiveArgs : Array Expr) : MetaM Unit :=
--- a/src/Lean/Meta/SizeOf.lean
+++ b/src/Lean/Meta/SizeOf.lean
@ -32,7 +32,7 @@ where
          loop (i+1) (insts.push inst)
    else
      k insts
-/-- 
+/--
  Let `motiveFVars` be free variables for each motive in a kernel recursor, and `minorFVars` the free variables for a minor premise.
  Then, return `true` is `fvar` (an element of `minorFVars`) corresponds to a recursive field.
  That is, there is a free variable `minorFVar` in `minorFVars` with type `... -> motive ... fvar` where `motive` is an element of `motiveFVars`.
@ -41,7 +41,7 @@ private def isRecField (motiveFVars : Array Expr) (minorFVars : Array Expr) (fva
  for minorFVar in minorFVars do
    let found ← forallTelescopeReducing (← inferType minorFVar) fun _ type =>
      return motiveFVars.contains type.getAppFn && type.appArg! == fvar
-    if found then 
+    if found then
      return true
  return false

@ -67,7 +67,7 @@ where
      forallTelescopeReducing (← inferType minorFVars[i]) fun xs _ =>
      forallBoundedTelescope (← inferType minorFVars'[i]) xs.size fun xs' _ => do
        let mut minor ← mkNumeral (mkConst ``Nat) 1
-        for x in xs, x' in xs' do   
+        for x in xs, x' in xs' do
          -- If `x` is a recursive field, we skip it since we use the inductive hypothesis occurring later
          unless (← isRecField motiveFVars xs x) do
            let xType ← inferType x
@ -77,28 +77,28 @@ where
                if ys.size > 0 then
                  -- ignore `x` because it is a function
                  return minor
-                else  
+                else
                  mkAdd minor x'
              else
-                try 
+                try
                  mkAdd minor (← mkAppM ``SizeOf.sizeOf #[x'])
                catch _ =>
-                  return minor 
-        minor ← mkLambdaFVars xs' minor        
-        trace[Meta.sizeOf]! "minor: {minor}"        
+                  return minor
+        minor ← mkLambdaFVars xs' minor
+        trace[Meta.sizeOf]! "minor: {minor}"
        loop (i+1) (minors.push minor)
    else
-      k minors 
+      k minors

 partial def mkSizeOfFn (recName : Name) : MetaM Unit := do
  trace[Meta.sizeOf]! "recName: {recName}"
  let recInfo : RecursorVal ← getConstInfoRec recName
  forallTelescopeReducing recInfo.type fun xs type =>
-    let levelParams := recInfo.lparams.tail! -- universe parameters for declaration being defined
-    let params := xs[:recInfo.nparams]
-    let motiveFVars := xs[recInfo.nparams : recInfo.nparams + recInfo.nmotives]
-    let minorFVars := xs[recInfo.getFirstMinorIdx : recInfo.getFirstMinorIdx + recInfo.nminors]
-    let indices := xs[recInfo.getFirstIndexIdx : recInfo.getFirstIndexIdx + recInfo.nindices]
+    let levelParams := recInfo.levelParams.tail! -- universe parameters for declaration being defined
+    let params := xs[:recInfo.numParams]
+    let motiveFVars := xs[recInfo.numParams : recInfo.numParams + recInfo.numMotives]
+    let minorFVars := xs[recInfo.getFirstMinorIdx : recInfo.getFirstMinorIdx + recInfo.numMinors]
+    let indices := xs[recInfo.getFirstIndexIdx : recInfo.getFirstIndexIdx + recInfo.numIndices]
    let major := xs[recInfo.getMajorIdx]
    let nat := mkConst ``Nat
    mkLocalInstances params fun localInsts =>
@ -106,7 +106,7 @@ partial def mkSizeOfFn (recName : Name) : MetaM Unit := do
      let us := levelOne :: levelParams.map mkLevelParam -- universe level parameters for `rec`-application
      let recFn := mkConst recName us
      let val := mkAppN recFn (params ++ motives)
-      forallBoundedTelescope (← inferType val) recInfo.nminors fun minorFVars' _ =>
+      forallBoundedTelescope (← inferType val) recInfo.numMinors fun minorFVars' _ =>
      mkSizeOfMinors motiveFVars minorFVars minorFVars' fun minors => do
        let sizeOfFnType ← mkForallFVars (params ++ localInsts ++ indices ++ #[major]) nat
        let val := mkAppN val (minors ++ indices ++ #[major])
--- a/src/Lean/Meta/Tactic/Cases.lean
+++ b/src/Lean/Meta/Tactic/Cases.lean
@ -19,7 +19,7 @@ def getInductiveUniverseAndParams (type : Expr) : MetaM (List Level × Array Exp
  matchConstInduct type.getAppFn (fun _ => throwInductiveTypeExpected type) fun val us =>
    let I      := type.getAppFn
    let Iargs  := type.getAppArgs
-    let params := Iargs.extract 0 val.nparams
+    let params := Iargs.extract 0 val.numParams
    pure (us, params)

 private def mkEqAndProof (lhs rhs : Expr) : MetaM (Expr × Expr) := do
@ -89,10 +89,10 @@ def generalizeIndices (mvarId : MVarId) (fvarId : FVarId) : MetaM GeneralizeIndi
    let fvarDecl ← getLocalDecl fvarId
    let type ← whnf fvarDecl.type
    type.withApp fun f args => matchConstInduct f (fun _ => throwTacticEx `generalizeIndices mvarId "inductive type expected") fun val _ => do
-      unless val.nindices > 0 do throwTacticEx `generalizeIndices mvarId "indexed inductive type expected"
-      unless args.size == val.nindices + val.nparams do throwTacticEx `generalizeIndices mvarId "ill-formed inductive datatype"
-      let indices := args.extract (args.size - val.nindices) args.size
-      let IA := mkAppN f (args.extract 0 val.nparams) -- `I A`
+      unless val.numIndices > 0 do throwTacticEx `generalizeIndices mvarId "indexed inductive type expected"
+      unless args.size == val.numIndices + val.numParams do throwTacticEx `generalizeIndices mvarId "ill-formed inductive datatype"
+      let indices := args.extract (args.size - val.numIndices) args.size
+      let IA := mkAppN f (args.extract 0 val.numParams) -- `I A`
      let IAType ← inferType IA
      forallTelescopeReducing IAType fun newIndices _ => do
      let newType := mkAppN IA newIndices
@ -132,7 +132,7 @@ structure Context where
  majorDecl        : LocalDecl
  majorTypeFn      : Expr
  majorTypeArgs    : Array Expr
-  majorTypeIndices : Array Expr := majorTypeArgs.extract (majorTypeArgs.size - inductiveVal.nindices) majorTypeArgs.size
+  majorTypeIndices : Array Expr := majorTypeArgs.extract (majorTypeArgs.size - inductiveVal.numIndices) majorTypeArgs.size

 private def mkCasesContext? (majorFVarId : FVarId) : MetaM (Option Context) := do
  let env ← getEnv
@ -142,7 +142,7 @@ private def mkCasesContext? (majorFVarId : FVarId) : MetaM (Option Context) := d
    let majorDecl ← getLocalDecl majorFVarId
    let majorType ← whnf majorDecl.type
    majorType.withApp fun f args => matchConstInduct f (fun _ => pure none) fun ival _ =>
-      if args.size != ival.nindices + ival.nparams then pure none
+      if args.size != ival.numIndices + ival.numParams then pure none
      else match env.find? (Name.mkStr ival.name "casesOn") with
        | ConstantInfo.defnInfo cval =>
          pure $ some {
@ -291,7 +291,7 @@ def cases (mvarId : MVarId) (majorFVarId : FVarId) (givenNames : Array (List Nam
      /- Remark: if caller does not need a `FVarSubst` (variable substitution), and `hasIndepIndices ctx` is true,
         then we can also use the simple case. This is a minor optimization, and we currently do not even
         allow callers to specify whether they want the `FVarSubst` or not. -/
-      if ctx.inductiveVal.nindices == 0 then
+      if ctx.inductiveVal.numIndices == 0 then
        -- Simple case
        inductionCasesOn mvarId majorFVarId givenNames useUnusedNames ctx
      else
--- a/src/Lean/Meta/Tactic/Constructor.lean
+++ b/src/Lean/Meta/Tactic/Constructor.lean
@ -16,11 +16,11 @@ def existsIntro (mvarId : MVarId) (w : Expr) : MetaM MVarId := do
    matchConstStruct target.getAppFn
      (fun _ => throwTacticEx `exists mvarId "target is not an inductive datatype with one constructor")
      fun ival us cval => do
-        if cval.nfields < 2 then
+        if cval.numFields < 2 then
          throwTacticEx `exists mvarId "constructor must have at least two fields"
-        let ctor := mkAppN (Lean.mkConst cval.name us) target.getAppArgs[:cval.nparams]
+        let ctor := mkAppN (Lean.mkConst cval.name us) target.getAppArgs[:cval.numParams]
        let ctorType ← inferType ctor
-        let (mvars, _, _) ← forallMetaTelescopeReducing ctorType (some (cval.nfields-2))
+        let (mvars, _, _) ← forallMetaTelescopeReducing ctorType (some (cval.numFields-2))
        let f := mkAppN ctor mvars
        checkApp f w
        let [mvarId] ← apply mvarId <| mkApp f w
--- a/src/Lean/Meta/Tactic/Injection.lean
+++ b/src/Lean/Meta/Tactic/Injection.lean
@ -42,7 +42,7 @@ def injectionCore (mvarId : MVarId) (fvarId : FVarId) : MetaM InjectionResultCor
            let newMVar ← mkFreshExprSyntheticOpaqueMVar newTarget tag
            assignExprMVar mvarId (mkApp val newMVar)
            let mvarId ← tryClear newMVar.mvarId! fvarId
-            pure $ InjectionResultCore.subgoal mvarId aCtor.nfields
+            pure $ InjectionResultCore.subgoal mvarId aCtor.numFields
          | _ => throwTacticEx `injection mvarId "ill-formed noConfusion auxiliary construction"
      | _, _ => throwTacticEx `injection mvarId "equality of constructor applications expected"

--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@ -75,10 +75,10 @@ private def toCtorWhenK (recVal : RecursorVal) (major : Expr) : MetaM (Option Ex
  let majorTypeI := majorType.getAppFn
  if !majorTypeI.isConstOf recVal.getInduct then
    pure none
-  else if majorType.hasExprMVar && majorType.getAppArgs[recVal.nparams:].any Expr.hasExprMVar then
+  else if majorType.hasExprMVar && majorType.getAppArgs[recVal.numParams:].any Expr.hasExprMVar then
    pure none
  else do
-    let (some newCtorApp) ← mkNullaryCtor majorType recVal.nparams | pure none
+    let (some newCtorApp) ← mkNullaryCtor majorType recVal.numParams | pure none
    let newType ← inferType newCtorApp
    if (← isDefEq majorType newType) then
      pure newCtorApp
@ -98,12 +98,12 @@ private def reduceRec {α} (recVal : RecursorVal) (recLvls : List Level) (recArg
    match getRecRuleFor recVal major with
    | some rule =>
      let majorArgs := major.getAppArgs
-      if recLvls.length != recVal.lparams.length then
+      if recLvls.length != recVal.levelParams.length then
        failK ()
      else
-        let rhs := rule.rhs.instantiateLevelParams recVal.lparams recLvls
+        let rhs := rule.rhs.instantiateLevelParams recVal.levelParams recLvls
        -- Apply parameters, motives and minor premises from recursor application.
-        let rhs := mkAppRange rhs 0 (recVal.nparams+recVal.nmotives+recVal.nminors) recArgs
+        let rhs := mkAppRange rhs 0 (recVal.numParams+recVal.numMotives+recVal.numMinors) recArgs
        /- The number of parameters in the constructor is not necessarily
           equal to the number of parameters in the recursor when we have
           nested inductive types. -/
@ -292,7 +292,7 @@ def project? (e : Expr) (i : Nat) : MetaM (Option Expr) := do
  let e ← whnf e
  matchConstCtor e.getAppFn (fun _ => pure none) fun ctorVal _ =>
    let numArgs := e.getAppNumArgs
-    let idx := ctorVal.nparams + i
+    let idx := ctorVal.numParams + i
    if idx < numArgs then
      pure (some (e.getArg! idx))
    else
--- a/src/Lean/Parser/Extension.lean
+++ b/src/Lean/Parser/Extension.lean
@ -422,7 +422,7 @@ def declareBuiltinParser (env : Environment) (addFnName : Name) (catName : Name)
  let name := `_regBuiltinParser ++ declName
  let type := mkApp (mkConst `IO) (mkConst `Unit)
  let val  := mkAppN (mkConst addFnName) #[toExpr catName, toExpr declName, mkConst declName, mkNatLit prio]
-  let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque,
+  let decl := Declaration.defnDecl { name := name, levelParams := [], type := type, value := val, hints := ReducibilityHints.opaque,
                                     safety := DefinitionSafety.safe }
  match env.addAndCompile {} decl with
  -- TODO: pretty print error
--- a/src/Lean/ParserCompiler.lean
+++ b/src/Lean/ParserCompiler.lean
@ -82,7 +82,7 @@ partial def compileParserExpr (e : Expr) : MetaM Expr := do
            let paramTy ← replaceParserTy ctx <$> inferType param
            pure $ mkForall `_ BinderInfo.default paramTy ty
        let decl := Declaration.defnDecl {
-          name := c', lparams := [],
+          name := c', levelParams := [],
          type := ty, value := value, hints := ReducibilityHints.opaque, safety := DefinitionSafety.safe }
        let env ← getEnv
        let env ← match env.addAndCompile {} decl with
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@ -454,14 +454,14 @@ def delabStructureInstance : Delab := whenPPOption getPPStructureInstances do
  /- If implicit arguments should be shown, and the structure has parameters, we should not
     pretty print using { ... }, because we will not be able to see the parameters. -/
  let explicit ← getPPOption getPPExplicit
-  guard !(explicit && s.nparams > 0)
+  guard !(explicit && s.numParams > 0)
  let fieldNames := getStructureFields env s.induct
  let (_, fields) ← withAppFnArgs (pure (0, #[])) fun ⟨idx, fields⟩ => do
-      if idx < s.nparams then
+      if idx < s.numParams then
        pure (idx + 1, fields)
      else
        let val ← delab
-        let field ← `(structInstField|$(mkIdent <| fieldNames.get! (idx - s.nparams)):ident := $val)
+        let field ← `(structInstField|$(mkIdent <| fieldNames.get! (idx - s.numParams)):ident := $val)
        pure (idx + 1, fields.push field)
  let lastField := fields[fields.size - 1]
  let fields := fields.pop
--- a/src/Lean/Structure.lean
+++ b/src/Lean/Structure.lean
@ -37,42 +37,42 @@ def deinternalizeFieldName : Name → Name

 def getStructureCtor (env : Environment) (constName : Name) : ConstructorVal :=
  match env.find? constName with
-  | some (ConstantInfo.inductInfo { nparams := nparams, isRec := false, ctors := [ctorName], .. }) =>
+  | some (ConstantInfo.inductInfo { isRec := false, ctors := [ctorName], .. }) =>
    match env.find? ctorName with
    | some (ConstantInfo.ctorInfo val) => val
    | _ => panic! "ill-formed environment"
  | _ => panic! "structure expected"

-private def getStructureFieldsAux (nparams : Nat) : Nat → Expr → Array Name → Array Name
+private def getStructureFieldsAux (numParams : Nat) : Nat → Expr → Array Name → Array Name
  | i, Expr.forallE n d b _, fieldNames =>
-    if i < nparams then
-      getStructureFieldsAux nparams (i+1) b fieldNames
+    if i < numParams then
+      getStructureFieldsAux numParams (i+1) b fieldNames
    else
-      getStructureFieldsAux nparams (i+1) b <| fieldNames.push <| deinternalizeFieldName n
+      getStructureFieldsAux numParams (i+1) b <| fieldNames.push <| deinternalizeFieldName n
  | _, _, fieldNames => fieldNames

 -- TODO: fix. See comment in the beginning of the file
 def getStructureFields (env : Environment) (structName : Name) : Array Name :=
  let ctor := getStructureCtor env structName;
-  getStructureFieldsAux ctor.nparams 0 ctor.type #[]
+  getStructureFieldsAux ctor.numParams 0 ctor.type #[]

-private def isSubobjectFieldAux (nparams : Nat) (target : Name) : Nat → Expr → Option Name
+private def isSubobjectFieldAux (numParams : Nat) (target : Name) : Nat → Expr → Option Name
  | i, Expr.forallE n d b _ =>
-    if i < nparams then
-      isSubobjectFieldAux nparams target (i+1) b
+    if i < numParams then
+      isSubobjectFieldAux numParams target (i+1) b
    else if n == target then
      match d.getAppFn with
      | Expr.const parentStructName _ _ => some parentStructName
      | _ => panic! "ill-formed structure"
    else
-      isSubobjectFieldAux nparams target (i+1) b
+      isSubobjectFieldAux numParams target (i+1) b
  | _, _ => none

 -- TODO: fix. See comment in the beginning of the file
 /-- If `fieldName` represents the relation to a parent structure `S`, return `S` -/
 def isSubobjectField? (env : Environment) (structName : Name) (fieldName : Name) : Option Name :=
  let ctor := getStructureCtor env structName;
-  isSubobjectFieldAux ctor.nparams (mkInternalSubobjectFieldName fieldName) 0 ctor.type
+  isSubobjectFieldAux ctor.numParams (mkInternalSubobjectFieldName fieldName) 0 ctor.type

 /-- Return immediate parent structures -/
 def getParentStructures (env : Environment) (structName : Name) : Array Name :=
@ -100,10 +100,10 @@ def getStructureFieldsFlattened (env : Environment) (structName : Name) : Array
  getStructureFieldsFlattenedAux env structName #[]

 -- TODO: fix. See comment in the beginning of the file
-private def hasProjFn (env : Environment) (structName : Name) (nparams : Nat) : Nat → Expr → Bool
+private def hasProjFn (env : Environment) (structName : Name) (numParams : Nat) : Nat → Expr → Bool
  | i, Expr.forallE n d b _ =>
-    if i < nparams then
-      hasProjFn env structName nparams (i+1) b
+    if i < numParams then
+      hasProjFn env structName numParams (i+1) b
    else
      let fullFieldName := structName ++ deinternalizeFieldName n;
      env.isProjectionFn fullFieldName
@ -118,7 +118,7 @@ private def hasProjFn (env : Environment) (structName : Name) (nparams : Nat) :
 def isStructure (env : Environment) (constName : Name) : Bool :=
  if isStructureLike env constName then
    let ctor := getStructureCtor env constName;
-    hasProjFn env constName ctor.nparams 0 ctor.type
+    hasProjFn env constName ctor.numParams 0 ctor.type
  else
    false

--- a/src/Lean/Util/Recognizers.lean
+++ b/src/Lean/Util/Recognizers.lean
@ -84,7 +84,7 @@ def isConstructorApp? (env : Environment) (e : Expr) : Option ConstructorVal :=
  | _ =>
    match e.getAppFn with
    | Expr.const n _ _ => match getConstructorVal? env n with
-      | some v => if v.nparams + v.nfields == e.getAppNumArgs then some v else none
+      | some v => if v.numParams + v.numFields == e.getAppNumArgs then some v else none
      | none   => none
    | _ => none

@ -104,7 +104,7 @@ def constructorApp? (env : Environment) (e : Expr) : Option (ConstructorVal × A
    match e.getAppFn with
    | Expr.const n _ _ => do
      let v ← getConstructorVal? env n
-      if v.nparams + v.nfields == e.getAppNumArgs then
+      if v.numParams + v.numFields == e.getAppNumArgs then
        pure (v, e.getAppArgs)
      else
        none
--- a/tests/lean/run/depElim1.lean
+++ b/tests/lean/run/depElim1.lean
@ -28,7 +28,7 @@ inductive ArrayLit4 {α : Sort u} (a b c d : α) : Type u | mk : ArrayLit4 a b c
 private def getConstructorVal (ctorName : Name) (fn : Expr) (args : Array Expr) : MetaM (Option (ConstructorVal × Expr × Array Expr)) := do
 let env ← getEnv
 match env.find? ctorName with
-| some (ConstantInfo.ctorInfo v) => if args.size == v.nparams + v.nfields then return some (v, fn, args) else return none
+| some (ConstantInfo.ctorInfo v) => if args.size == v.numParams + v.numFields then return some (v, fn, args) else return none
 | _                              => return none

 private def constructorApp? (e : Expr) : MetaM (Option (ConstructorVal × Expr × Array Expr)) := do
@ -79,8 +79,8 @@ partial def mkPattern : Expr → MetaM Pattern
      match r? with
      | none      => throwError "unexpected pattern"
      | some (cval, fn, args) =>
-        let params := args.extract 0 cval.nparams
-        let fields := args.extract cval.nparams args.size
+        let params := args.extract 0 cval.numParams
+        let fields := args.extract cval.numParams args.size
        let pats ← fields.toList.mapM mkPattern
        return Pattern.ctor cval.name fn.constLevels! params.toList pats

--- a/tests/lean/run/meta2.lean
+++ b/tests/lean/run/meta2.lean
@ -242,13 +242,14 @@ do print "----- tst14 -----";

 def tst15 : MetaM Unit :=
 do print "----- tst15 -----";
-   let inst ← mkAdd nat;
+   let inst ← _root_.mkAdd nat;
   let r ← synthInstance inst;
   print r;
   pure ()

 #eval tst15

+
 def tst16 : MetaM Unit :=
 do print "----- tst16 -----";
   let prod ← mkProd nat nat;
--- a/tests/lean/run/toExpr.lean
+++ b/tests/lean/run/toExpr.lean
@ -6,12 +6,12 @@ unsafe def test {α : Type} [ToString α] [ToExpr α] [BEq α] (a : α) : CoreM
 let env ← getEnv;
 let auxName := `_toExpr._test;
 let decl := Declaration.defnDecl {
-  name     := auxName,
-  lparams  := [],
-  value    := toExpr a,
-  type     := toTypeExpr α,
-  hints    := ReducibilityHints.abbrev,
-  safety   := DefinitionSafety.safe
+  name        := auxName,
+  levelParams := [],
+  value       := toExpr a,
+  type        := toTypeExpr α,
+  hints       := ReducibilityHints.abbrev,
+  safety      := DefinitionSafety.safe
 };
 IO.println (toExpr a);
 (match env.addAndCompile {} decl with