Documentation for attributes

Stream: lean4

[Ioannis Konstantoulas]

Do we have a place where the various @[x] are documented? I don't know what things like specialize, private, implemented_by, etc. are. Also interested in the difference between inline, always_inline, macro_inline, etc.

[Eric Wieser]

If you hover over them in vscode, you should get docstrings

[Ioannis Konstantoulas]

Eric Wieser said:

If you hover over them in vscode, you should get docstrings

Huh, that is weird; I swear I had tried to do this before and didn't work. Thanks!

[Alexandre Rademaker]

It does not work for me. I am trying to understand the difference between @[inline] and partial def

[Alexandre Rademaker]

OK, it worked in the Main file, but not all files. Anyway, the docstring does not mention the inline attribute.

[Jireh Loreaux]

There's also #help attr inline, although admittedly the documentation is very sparse, and somewhat circular.

[Alexandre Rademaker]

Hum, #help is not working for me! I am using Lean (version 4.4.0, commit ca7d6dadb9e1, Release)

[Kyle Miller]

#help attr is a mathlib extension, defined in Mathlib.Tactic.HelpCmd