1
$\begingroup$

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?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
4
$\begingroup$

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
Improve this answer
$\endgroup$
2
  • $\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$
    – Alex Byard
    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$
    – damiano
    Commented May 30, 2023 at 15:52

Not the answer you're looking for? Browse other questions tagged or ask your own question.