diff --git a/src/Lean/Elab/Deriving/FromToJson.lean b/src/Lean/Elab/Deriving/FromToJson.lean index a986383e3b..7c4149c207 100644 --- a/src/Lean/Elab/Deriving/FromToJson.lean +++ b/src/Lean/Elab/Deriving/FromToJson.lean @@ -132,7 +132,6 @@ where let localDecl ← getLocalDecl x.fvarId! if !localDecl.userName.hasMacroScopes then userNames := userNames.push localDecl.userName - let xTy ← inferType x let a := mkIdent (← mkFreshUserName `a) identNames := identNames.push a let jsonAccess ← identNames.mapIdxM (fun idx _ => `(jsons[$(quote idx.val)]))