From 03e6572584098c54774290f673cc110bc5685124 Mon Sep 17 00:00:00 2001
From: Seppel3210 <34406239+Seppel3210@users.noreply.github.com>
Date: Thu, 22 Dec 2022 23:12:18 +0100
Subject: [PATCH] =?UTF-8?q?fix:=20mention=20(a=20:=20=CE=B1)=20=E2=86=92?=
 =?UTF-8?q?=20=CE=B2=20a=20notation=20in=20foundational=20types=20section?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 DocGen4/Output/FoundationalTypes.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/DocGen4/Output/FoundationalTypes.lean b/DocGen4/Output/FoundationalTypes.lean
index b1e00a7..7ece5c7 100644
--- a/DocGen4/Output/FoundationalTypes.lean
+++ b/DocGen4/Output/FoundationalTypes.lean
@@ -34,17 +34,19 @@ def foundationalTypes : BaseHtmlM Html := templateLiftExtends (baseHtml "Foundat
       <p>Note that these can also be written with the alternative notations:</p>
       <ul>
       <li><code>∀ a : α, β a</code>, conventionally used where <code>β a : Prop</code>.</li>
+      <li><code>(a : α) → β a</code></li>
       <li><code>α → γ</code>, possible only if <code>β a = γ</code> for all <code>a</code>.</li>
       </ul>
       <p>Lean also permits ASCII-only spellings of the three variants:</p>
       <ul>
       <li><code>Pi 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) -&gt; B a</code>, for <code>(a : α) → β a</code></li>
       <li><code>A -&gt; B</code>, for <code>α → β</code></li>
       </ul>
       <p>Note that despite not itself being a function, <code>(→)</code> is available as infix notation for
       <code>{"λ α β, α → β"}</code>.</p>    
-      -- TODO: instnaces for pi types 
+      -- TODO: instances for pi types 
     </main>
 
 end DocGen4.Output