search

leanprover-community / lean4game

Server to host lean games.
https://adam.math.hhu.de
GNU General Public License v3.0
199 stars 35 forks source link

Use Statement description as the default LemmaDoc for that new lemma introduced by `Statement` command #78

Closed abentkamp closed 1 year ago

abentkamp commented 1 year ago

Or copy the docstring...

joneugster commented 1 year ago

It is now using the statement description or displays missing. Further improvements are tracked in #51.