This is a rather simple question which I cannot find an answer to in the Lean 4 API or anywhere else online. What does the @[inherit_doc] attribute do?
$\begingroup$
$\endgroup$
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
2
The syntax is @[inherit_doc declaration_name]: it adds the doc-string of declaration_name to the following declaration.
In the example below, I assume that you use VSCode.
/-- I am a doc-string. -/
theorem hello : True := trivial
@[inherit_doc hello]
theorem byeDoc : True := trivial
theorem byeNoDoc : True := trivial
#check hello -- hover on name: see a doc-string
#check byeNoDoc -- hover on name: do not see a doc-string
#check byeDoc -- hover on name: see a doc-string
-
$\begingroup$ Ahh okay, so it allows you to carry on down those comments connected to the theorem. What about, say, in Data/Real/Basic when we claim the notation \mathbb{R}? It is preceeded with
@[inherit_doc]with no declaration name included. What is the function of the attribute in this case? $\endgroup$ Commented May 30, 2023 at 15:17 -
1$\begingroup$ This passes on the docs of the structure to the notation. In that case, you can hover over \R and see the doc-strings of the structure
Real. I do not know exactly under which circumstances, but the attribute makes an educated guess as to the provenance of the docs, when you do not specify it, failing if it finds no good target. $\endgroup$– damianoCommented May 30, 2023 at 15:52