From da55d737f3350c49ea163cc6518b668e66fed77a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Martin=20Dvo=C5=99=C3=A1k?= <martin.dvorak@matfyz.cz>
Date: Fri, 6 Dec 2024 11:23:04 +0100
Subject: [PATCH] typo (note that the space was not displayed)

---
 DocGen4/Output/FoundationalTypes.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/DocGen4/Output/FoundationalTypes.lean b/DocGen4/Output/FoundationalTypes.lean
index 3eb694e2..b15d53e7 100644
--- a/DocGen4/Output/FoundationalTypes.lean
+++ b/DocGen4/Output/FoundationalTypes.lean
@@ -39,7 +39,7 @@ def foundationalTypes : BaseHtmlM Html := templateLiftExtends (baseHtml "Foundat
       </ul>
       <p>Lean also permits ASCII-only spellings of the three variants:</p>
       <ul>
-      <li><code>forall a : A, B a</code> for <code>{"∀ a : α, β a"}</code></li>
+      <li><code>forall a : A, B a</code>, for <code>{"∀ a : α, β a"}</code></li>
       <li><code>{"(a : A) -> B a"}</code>, for <code>(a : α) → β a</code></li>
       <li><code>{"A -> B"}</code>, for <code>α → β</code></li>
       </ul>