phc/lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

remove docstring warning if TacticDoc is provided

Browse Source 
Fixes https://github.com/hhu-adam/NNG4/issues/21
This commit is contained in:
Alexander Bentkamp
2023-09-25 15:09:32 +02:00
parent c50517b5e6
commit 1d49535fcf
1 changed files with 5 additions and 5 deletions
Download Patch File Download Diff File Expand all files Collapse all files
server/GameServer/Commands.lean
+5 -5
View File
@@ -765,17 +765,17 @@ elab "MakeGame" : command => do
for item in inventoryTemplateExt.getState env do for item in inventoryTemplateExt.getState env do
let name := item.name let name := item.name
let docstring ← getDocstring env name item.type let content : String ← match item.content with
let content : String := match item.content with
| "" => | "" =>
-- If documentation is missing, try using the docstring instead. -- If documentation is missing, try using the docstring instead.
let docstring ← getDocstring env name item.type
match docstring with match docstring with
| some ds => s!"*(lean docstring)*\\\n{ds}" | some ds => pure s!"*(lean docstring)*\\\n{ds}"
| none => "(missing)" | none => pure "(missing)"
| template => | template =>
-- TODO: Process content template. -- TODO: Process content template.
-- TODO: Add information about inventory items -- TODO: Add information about inventory items
template.replace "[[mathlib_doc]]" pure $ template.replace "[[mathlib_doc]]"
s!"[mathlib doc](https://leanprover-community.github.io/mathlib4_docs/find/?pattern={name}#doc)" s!"[mathlib doc](https://leanprover-community.github.io/mathlib4_docs/find/?pattern={name}#doc)"
match item.type with match item.type with