Zulip Chat Archive

Stream: lean4

Topic: Documentation for attributes

Ioannis Konstantoulas (Oct 09 2023 at 13:48):

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 (Oct 09 2023 at 14:09):

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

Ioannis Konstantoulas (Oct 09 2023 at 14:15):

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!

Last updated: Dec 20 2023 at 11:08 UTC