diff --git a/src/Lean/Elab/Deriving/Basic.lean b/src/Lean/Elab/Deriving/Basic.lean
index 7beb00532f..b2030582d3 100644
--- a/src/Lean/Elab/Deriving/Basic.lean
+++ b/src/Lean/Elab/Deriving/Basic.lean
@@ -5,11 +5,10 @@ Authors: Leonardo de Moura
 -/
 import Lean.Elab.Command
 
-namespace Lean
-namespace Elab
+namespace Lean.Elab
 open Command
 
-def DerivingHandler := (typeNames : List Name) → CommandElabM Bool
+def DerivingHandler := (typeNames : Array Name) → CommandElabM Bool
 
 builtin_initialize derivingHandlersRef : IO.Ref (NameMap DerivingHandler) ← IO.mkRef {}
 
@@ -21,18 +20,25 @@ def registerBuiltinDerivingHandler (className : Name) (handler : DerivingHandler
     throw (IO.userError s!"failed to register deriving handler, a handler has already been registered for '{className}'")
   derivingHandlersRef.modify fun m => m.insert className handler
 
-def defaultHandler (className : Name) (typeNames : List Name) : CommandElabM Unit := do
-  throwError! "default handlers have not been implemented yet, {typeNames}"
+def defaultHandler (className : Name) (typeNames : Array Name) : CommandElabM Unit := do
+  throwError! "default handlers have not been implemented yet, class: '{className}' types: {typeNames}"
 
-def applyDerivingHandlers (className : Name) (typeNames : List Name) : CommandElabM Unit := do
+def applyDerivingHandlers (className : Name) (typeNames : Array Name) : CommandElabM Unit := do
   match (← derivingHandlersRef.get).find? className with
   | some handler =>
     unless (← handler typeNames) do
       defaultHandler className typeNames
   | none => defaultHandler className typeNames
 
+@[builtinCommandElab «deriving»] def elabDeriving : CommandElab
+  | `(deriving instance $[$classes],* for $[$declNames],*) => do
+     let classes ← classes.mapM (resolveGlobalConstNoOverload ·.getId)
+     let declNames ← declNames.mapM (resolveGlobalConstNoOverload ·.getId)
+     for cls in classes do
+       try
+         applyDerivingHandlers cls declNames
+       catch ex =>
+         logException ex
+  | _ => throwUnsupportedSyntax
 
-
-
-end Elab
-end Lean
+end Lean.Elab