From 1d49535fcf5de39a5201c33eb70ad1aafdc2ce76 Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Mon, 25 Sep 2023 15:09:32 +0200 Subject: [PATCH] remove docstring warning if TacticDoc is provided Fixes https://github.com/hhu-adam/NNG4/issues/21 --- server/GameServer/Commands.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean index 1b03b0a..a75d804 100644 --- a/server/GameServer/Commands.lean +++ b/server/GameServer/Commands.lean @@ -765,17 +765,17 @@ elab "MakeGame" : command => do for item in inventoryTemplateExt.getState env do 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. + let docstring ← getDocstring env name item.type match docstring with - | some ds => s!"*(lean docstring)*\\\n{ds}" - | none => "(missing)" + | some ds => pure s!"*(lean docstring)*\\\n{ds}" + | none => pure "(missing)" | template => -- TODO: Process content template. -- 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)" match item.type with