fix doc string

2 years ago · 6cd71c93fe
parent e7842bce82
commit 6cd71c93fe
1 changed files with 1 additions and 1 deletions
--- a/server/leanserver/GameServer/Commands.lean
+++ b/server/leanserver/GameServer/Commands.lean
@ -383,7 +383,7 @@ elab "OnlyDefinition" args:ident* : command => do
 /-- Documentation entry of a lemma. Example:

 ```
-LemmaDoc Nat.succ_pos as "succ_pos" in Nat "says `0 < n.succ`, etc."
+LemmaDoc Nat.succ_pos as "succ_pos" in "Nat" "says `0 < n.succ`, etc."
 ```

 * The first identifier is used in the commands `[New/Only/Disabled]Lemma`.