diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index 835975ecdb..3c21c569ac 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -513,11 +513,11 @@ private def elabStructureView (view : StructView) : TermElabM Unit := do
            The parameters `params` for these definitions must be marked as implicit, and all others as explicit. -/
         let lctx :=
           params.foldl (init := lctx) fun (lctx : LocalContext) (p : Expr) =>
-            lctx.updateBinderInfo p.fvarId! BinderInfo.implicit
+            lctx.setBinderInfo p.fvarId! BinderInfo.implicit
         let lctx :=
           fieldInfos.foldl (init := lctx) fun (lctx : LocalContext) (info : StructFieldInfo) =>
             if info.isFromParent then lctx -- `fromParent` fields are elaborated as let-decls, and are zeta-expanded when creating `_default`.
-            else lctx.updateBinderInfo info.fvar.fvarId! BinderInfo.default
+            else lctx.setBinderInfo info.fvar.fvarId! BinderInfo.default
         addDefaults lctx defaultAuxDecls
 
 /-
diff --git a/src/Lean/LocalContext.lean b/src/Lean/LocalContext.lean
index c9d48926d2..4b7a4963a4 100644
--- a/src/Lean/LocalContext.lean
+++ b/src/Lean/LocalContext.lean
@@ -74,11 +74,11 @@ def setValue : LocalDecl → Expr → LocalDecl
   | ldecl idx id n t _ nd, v => ldecl idx id n t v nd
   | d, _                     => d
 
-def updateUserName : LocalDecl → Name → LocalDecl
+def setUserName : LocalDecl → Name → LocalDecl
   | cdecl index id _ type bi,     userName => cdecl index id userName type bi
   | ldecl index id _ type val nd, userName => ldecl index id userName type val nd
 
-def updateBinderInfo : LocalDecl → BinderInfo → LocalDecl
+def setBinderInfo : LocalDecl → BinderInfo → LocalDecl
   | cdecl index id n type _,  bi => cdecl index id n type bi
   | ldecl .., _                  => panic! "unexpected let declaration"
 
@@ -214,7 +214,7 @@ def lastDecl (lctx : LocalContext) : Option LocalDecl :=
 
 def setUserName (lctx : LocalContext) (fvarId : FVarId) (userName : Name) : LocalContext :=
   let decl := lctx.get! fvarId
-  let decl := decl.updateUserName userName
+  let decl := decl.setUserName userName
   { fvarIdToDecl := lctx.fvarIdToDecl.insert decl.fvarId decl,
     decls        := lctx.decls.set decl.index decl }
 
@@ -225,7 +225,7 @@ def renameUserName (lctx : LocalContext) (fromName : Name) (toName : Name) : Loc
     match lctx.findFromUserName? fromName with
     | none      => lctx
     | some decl =>
-      let decl := decl.updateUserName toName;
+      let decl := decl.setUserName toName;
       { fvarIdToDecl := map.insert decl.fvarId decl,
         decls        := decls.set decl.index decl }
 
@@ -243,8 +243,8 @@ def renameUserName (lctx : LocalContext) (fromName : Name) (toName : Name) : Loc
       { fvarIdToDecl := map.insert decl.fvarId decl,
         decls        := decls.set decl.index decl }
 
-def updateBinderInfo (lctx : LocalContext) (fvarId : FVarId) (bi : BinderInfo) : LocalContext :=
-  modifyLocalDecl lctx fvarId fun decl => decl.updateBinderInfo bi
+def setBinderInfo (lctx : LocalContext) (fvarId : FVarId) (bi : BinderInfo) : LocalContext :=
+  modifyLocalDecl lctx fvarId fun decl => decl.setBinderInfo bi
 
 @[export lean_local_ctx_num_indices]
 def numIndices (lctx : LocalContext) : Nat :=
diff --git a/src/Lean/Meta/Check.lean b/src/Lean/Meta/Check.lean
index a10e0d7ff5..868bea313b 100644
--- a/src/Lean/Meta/Check.lean
+++ b/src/Lean/Meta/Check.lean
@@ -150,10 +150,10 @@ where
       xs.forM fun x => do
         let xDecl ← getFVarLocalDecl x;
         match xDecl with
-        | LocalDecl.cdecl _ _ _ t _ =>
+        | LocalDecl.cdecl (type := t) .. =>
           ensureType t
           checkAux t
-        | LocalDecl.ldecl _ _ _ t v _ =>
+        | LocalDecl.ldecl (type := t) (value := v) .. =>
           ensureType t
           checkAux t
           let vType ← inferType v
diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index 9c72c1ff97..5390aab1b6 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -728,7 +728,7 @@ partial def check
     | Expr.fvar fvarId ..  =>
       if mvarDecl.lctx.contains fvarId then true
       else match lctx.find? fvarId with
-        | some (LocalDecl.ldecl _ _ _ _ v _) => false -- need expensive CheckAssignment.check
+        | some (LocalDecl.ldecl (value := v) ..) => false -- need expensive CheckAssignment.check
         | _ =>
           if fvars.any $ fun x => x.fvarId! == fvarId then true
           else false -- We could throw an exception here, but we would have to use ExceptM. So, we let CheckAssignment.check do it
diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index c5ed7dc24f..c7ec5d2bbc 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -217,7 +217,7 @@ end
     let decl ← getLocalDecl fvarId
     match decl with
     | LocalDecl.cdecl .. => return e
-    | LocalDecl.ldecl _ _ _ _ v nonDep =>
+    | LocalDecl.ldecl (value := v) (nonDep := nonDep) .. =>
       let cfg ← getConfig
       if nonDep && !cfg.zetaNonDep then
         return e
diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean
index 158fa679e9..8bd8f9ab98 100644
--- a/src/Lean/MetavarContext.lean
+++ b/src/Lean/MetavarContext.lean
@@ -676,8 +676,8 @@ end DependsOn
   depends on a free variable `x` s.t. `p x` is `true`. -/
 @[inline] def findLocalDeclDependsOn (mctx : MetavarContext) (localDecl : LocalDecl) (p : FVarId → Bool) : Bool :=
   match localDecl with
-  | LocalDecl.cdecl _ _ _ type _       => findExprDependsOn mctx type p
-  | LocalDecl.ldecl _ _ _ type value _ => (DependsOn.main mctx p type <||> DependsOn.main mctx p value).run' {}
+  | LocalDecl.cdecl (type := t) ..  => findExprDependsOn mctx t p
+  | LocalDecl.ldecl (type := t) (value := v) .. => (DependsOn.main mctx p t <||> DependsOn.main mctx p v).run' {}
 
 def exprDependsOn (mctx : MetavarContext) (e : Expr) (fvarId : FVarId) : Bool :=
   findExprDependsOn mctx e fun fvarId' => fvarId == fvarId'