add basic infos to inventory

leanprover-community · Jun 18, 2024 · 67090f5 · 67090f5
1 parent 2896237
commit 67090f5
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 1 deletion.
diff --git a/client/src/components/inventory.tsx b/client/src/components/inventory.tsx
@@ -229,6 +229,16 @@ export function Documentation() {
     <h1 className="doc">{docTile.displayName}</h1>
     <p><code>{docEntry.data?.statement}</code></p>
     <Markdown>{t(docEntry.data?.content, {ns: gameId})}</Markdown>
+    {/* TODO: The condition below should be updated so that the section
+    is displayed whenever it's non-empty. */}
+    {docTile.proven && <>
+        <h2>Further details</h2>
+        <ul>
+          {docTile.proven && <li>Proven in: <a href={`#/${gameId}/world/${docTile.world}/level/${docTile.level}`}>{docTile.world} level {docTile.level}</a></li>}
+        </ul>
+      </>
+    }
+
   </div>
 }
 

diff --git a/server/GameServer/EnvExtensions.lean b/server/GameServer/EnvExtensions.lean
@@ -109,7 +109,7 @@ structure InventoryTile where
   hidden := false
   /-- hover text -/
   altTitle : String := default
-deriving ToJson, FromJson, Repr, Inhabited
+deriving ToJson, FromJson, Repr, Inhabited, BEq
 
 def InventoryItem.toTile (item : InventoryItem) : InventoryTile := {
       name := item.name,