From efb96ab8fc0467aaebcdb9384661d194eda819ac Mon Sep 17 00:00:00 2001
From: cannorin <cannorin@users.noreply.github.com>
Date: Thu, 20 Feb 2025 00:25:10 +0900
Subject: [PATCH] kripke: improve rules

---
 apps/web/src/lib/components/katex.svelte |  6 +++---
 apps/web/src/routes/kripke/rules.svelte  | 20 ++++++++++++++++----
 2 files changed, 19 insertions(+), 7 deletions(-)

diff --git a/apps/web/src/lib/components/katex.svelte b/apps/web/src/lib/components/katex.svelte
index c2c3e48..12c590a 100644
--- a/apps/web/src/lib/components/katex.svelte
+++ b/apps/web/src/lib/components/katex.svelte
@@ -3,7 +3,7 @@ import katex from "katex";
 import "katex/dist/katex.min.css";
 import type { HTMLAttributes } from "svelte/elements";
 
-export interface KatexProps extends HTMLAttributes<HTMLDivElement> {
+export interface KatexProps extends HTMLAttributes<HTMLSpanElement> {
   displayMode?: boolean;
   math: string;
 }
@@ -15,6 +15,6 @@ let katexString = $derived.by(() =>
 );
 </script>
 
-<div {...rest}>
+<span {...rest}>
   {@html katexString}
-</div>
+</span>
diff --git a/apps/web/src/routes/kripke/rules.svelte b/apps/web/src/routes/kripke/rules.svelte
index 5f6a430..3f856d2 100644
--- a/apps/web/src/routes/kripke/rules.svelte
+++ b/apps/web/src/routes/kripke/rules.svelte
@@ -1,14 +1,22 @@
 <script lang="ts">
+import Katex from "$lib/components/katex.svelte";
 import LuHeart from "lucide-svelte/icons/heart";
+
+const frame = "\\footnotesize \\mathcal{F} = \\left<W, R\\right>";
+const numberConstraint = "\\footnotesize |W| = 4";
+const f = "\\footnotesize \\mathcal{F}";
+const validCount =
+  "\\footnotesize \\mathrm{N}(\\varphi) = \\bigl| \\Set{ w \\in W | \\forall \\mathop{\\Vdash}\\, (w \\Vdash \\varphi) } \\bigr|";
 </script>
 
 <h2>Rules</h2>
 <ul>
   <li>
-    A Kripke frame with 4 worlds is generated.
+    A Kripke frame with 4 worlds is generated:
+    <Katex math={frame} />, where <Katex math={numberConstraint} />.
   </li>
   <li>
-    The game tells you how many accessibility relations are in the frame, but not the exact shape of it.
+    The game tells you how many accessibility relations are in the frame <Katex math={f} />, but not the exact shape of it.
   </li>
   <li>
     You have a total of 10 moves <span class="inline-flex items-center max-w-fit">(<LuHeart aria-label="♡" size=12 class="mt-1"/>)</span>.
@@ -16,11 +24,15 @@ import LuHeart from "lucide-svelte/icons/heart";
     <ul>
       <li>
         Enter a modal formula.
-        The game tells you in how many worlds the formula is valid (for every valuation).
+        The game tells you in how many worlds the formula is valid.
+        In other words, it tells you the following natural number:
+        <div>
+          <Katex math={validCount} />
+        </div>
       </li>
       <li>
         Guess the Kripke frame.
-        If your frame is equal or isomorphic to the secret frame, you win.
+        If your frame is equal or isomorphic to the secret frame <Katex math={f} />, you win.
       </li>
     </ul>
   </li>