doc: update obsolete docstring for registerDerivingHandler (#9152)

This PR fixes an obsolete docstring for `registerDerivingHandler`
This commit is contained in:
David Thrane Christiansen 2025-07-02 06:03:00 +02:00 committed by GitHub
parent 094dd588d6
commit 8c0cff83bd
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

View file

@ -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")