Tactics for restate propositions

Stream: Is there code for X?

[SnO2WMaN]

In our project, we thought cumbersome to generate documentation each repository, so create repository for generating documentation across repos (like mathlib). Now in this repository we'd like to restate some important result/theorems as summary, is there any such tactic? I expect this tactic (such below): on a page by doc-gen re-show the content of theorem and comments but essentially acts as a redirect.

import Incompleteness.Arith.First
import Incompleteness.Arith.Second

restate LO.FirstOrder.Arith.goedel_first_incompleteness

restate LO.FirstOrder.Arith.goedel_second_incompleteness

[Johan Commelin]

See docs#recall

[Johan Commelin]

Ooops that didn't work

[Johan Commelin]

test/Recall.lean should help

[SnO2WMaN]

recall is works on editor, but not in doc-gen's documentation (nothing to view...)

• https://github.com/FormalizedFormalLogic/Summary/blob/bb7c798b83404dcb69c87560106bd9ced5c422aa/Summary/Modal.lean
• https://formalizedformallogic.github.io/Summary/Summary/Modal.html