diff --git a/src/Lean/Elab/Deriving/Basic.lean b/src/Lean/Elab/Deriving/Basic.lean index a93f5b0602..15881c1bbe 100644 --- a/src/Lean/Elab/Deriving/Basic.lean +++ b/src/Lean/Elab/Deriving/Basic.lean @@ -67,11 +67,12 @@ def DerivingHandler := (typeNames : Array Name) → CommandElabM Bool builtin_initialize derivingHandlersRef : IO.Ref (NameMap (List DerivingHandler)) ← IO.mkRef {} -/-- A `DerivingHandler` is called on the fully qualified names of all types it is running for -as well as the syntax of a `with` argument, if present. +/-- +Registers a deriving handler for a class. This function should be called in an `initialize` block. -For example, `deriving instance Foo with fooArgs for Bar, Baz` invokes -``fooHandler #[`Bar, `Baz] `(fooArgs)``. -/ +A `DerivingHandler` is called on the fully qualified names of all types it is running for. For +example, `deriving instance Foo for Bar, Baz` invokes ``fooHandler #[`Bar, `Baz]``. +-/ def registerDerivingHandler (className : Name) (handler : DerivingHandler) : IO Unit := do unless (← initializing) do throw (IO.userError "failed to register deriving handler, it can only be registered during initialization")