r
/
bookshelf-doc
mirror of https://github.com/jrpotter/bookshelf-doc
1
Fork 0
Code Issues Packages Projects Releases Wiki Activity

fix: mention (a : α) → β a notation in foundational types section

main
Seppel3210 2022-12-22 23:12:18 +01:00 committed by Henrik Böving
parent 345036e800
commit 03e6572584
1 changed files with 3 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
DocGen4/Output/FoundationalTypes.lean
View File

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