Allow docstring for command

Stream: metaprogramming / tactics

[Shreyas Srinivas]

Suppose I define a new command. How do I allow docstring comments to treat this command as a declaration (it is adding them). More context here:
https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/Refactoring.20with.20Euqation.20Command/near/474930942

[Shreyas Srinivas]

More specifically for this command : https://github.com/teorth/equational_theories/blob/1f2b19606c96d6550c8d8bbce087e6d09cc5e377/equational_theories/EquationsCommand.lean#L11

[Yury G. Kudryashov]

You can see how, e.g., Batteries.Tactic.Alias.alias does it.

[Yury G. Kudryashov]

It looks like the key is mods:declModifiers in

elab (name := alias) mods:declModifiers "alias " alias:ident " := " name:ident : command =>
  Command.liftTermElabM do
    let declMods ← elabModifiers mods
    -- Create a decl named `declName`
    addDocString' declName declMods.docString?

[Shreyas Srinivas]

That worked. Thanks