add command `HideDoc`. - Githubissues

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

Closed joneugster closed 1 year ago

joneugster commented 1 year ago

Provide a way to add an object (lemma/tactic) without a inventory entry appearing.

One option would be

NewTactic repeat
HiddenDoc repeat

Another one would be NewHiddenTactic repeat