bookshelf-doc/DocGen4/Output/FoundationalTypes.lean

53 lines
2.4 KiB
Plaintext
Raw Blame History

This file contains ambiguous Unicode characters!

This file contains ambiguous Unicode characters that may be confused with others in your current locale. If your use case is intentional and legitimate, you can safely ignore this warning. Use the Escape button to highlight these characters.

import DocGen4.Output.Template
import DocGen4.Output.Inductive
namespace DocGen4.Output
open scoped DocGen4.Jsx
def foundationalTypes : BaseHtmlM Html := templateLiftExtends (baseHtml "Foundational Types") do
pure <|
<main>
<a id="top"></a>
<h1>Foundational Types</h1>
<p>Some of Lean's types are not defined in any Lean source files (even the <code>prelude</code>) since they come from its foundational type theory. This page provides basic documentation for these types.</p>
<p>For a more in-depth explanation of Lean's type theory, refer to
<a href="https://leanprover.github.io/theorem_proving_in_lean4/dependent_type_theory.html">TPiL</a>.</p>
<h2 id="codesort-ucode"><code>Sort u</code></h2>
<p><code>Sort u</code> is the type of types in Lean, and <code>Sort u : Sort (u + 1)</code>.</p>
{← instancesForToHtml `_builtin_sortu}
<h2 id="codetype-ucode"><code>Type u</code></h2>
<p><code>Type u</code> is notation for <code>Sort (u + 1)</code>.</p>
{← instancesForToHtml `_builtin_typeu}
<h2 id="codepropcode"><code>Prop</code></h2>
<p><code>Prop</code> is notation for <code>Sort 0</code>.</p>
{← instancesForToHtml `_builtin_prop}
<h2 id="pi-types-codeπ-a--α-β-acode">Pi types, <code>{"Π a : α, β a"}</code></h2>
<p>The type of dependent functions is known as a pi type.
Non-dependent functions and implications are a special case.</p>
<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: instances for pi types
</main>
end DocGen4.Output