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?
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