-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathfoundational_types.html
More file actions
4 lines (4 loc) · 3.66 KB
/
foundational_types.html
File metadata and controls
4 lines (4 loc) · 3.66 KB
1
2
3
4
<html lang="en"><head><meta charset="UTF-8"></meta><meta name="viewport" content="width=device-width, initial-scale=1"></meta><link rel="stylesheet" href="./style.css"></link><link rel="icon" href="./favicon.svg"></link><link rel="mask-icon" href="./favicon.svg" color="#000000"></link><link rel="prefetch" href=".//declarations/declaration-data.bmp" as="image"></link><title>Foundational Types</title><script defer="true" src="./mathjax-config.js"></script><script defer="true" src="https://cdnjs.cloudflare.com/polyfill/v3/polyfill.min.js?features=es6"></script><script defer="true" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script><script>const SITE_ROOT="./";</script><script type="module" src="./jump-src.js"></script><script type="module" src="./search.js"></script><script type="module" src="./expand-nav.js"></script><script type="module" src="./how-about.js"></script><script type="module" src="./instances.js"></script><script type="module" src="./importedBy.js"></script></head><body><input id="nav_toggle" type="checkbox"></input><header><h1><label for="nav_toggle"></label><span>Documentation</span></h1><h2 class="header_filename break_within"><span class="name">Foundational Types</span></h2><form id="search_form"><input type="text" name="q" autocomplete="off"></input> <button id="search_button" onclick="javascript: form.action='./search.html';">Search</button></form></header><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><details id="instances-for-list-_builtin_sortu" class="instances-for-list"><summary>Instances For</summary><ul class="instances-for-enum"></ul></details><h2 id="codetype-ucode"><code>Type u</code></h2><p><code>Type u</code>is notation for <code>Sort (u + 1)</code>.</p><details id="instances-for-list-_builtin_typeu" class="instances-for-list"><summary>Instances For</summary><ul class="instances-for-enum"></ul></details><h2 id="codepropcode"><code>Prop</code></h2><p><code>Prop</code>is notation for <code>Sort 0</code>.</p><details id="instances-for-list-_builtin_prop" class="instances-for-list"><summary>Instances For</summary><ul class="instances-for-enum"></ul></details><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>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><p>Note that despite not itself being a function, <code>(→)</code>is available as infix notation for
<code>fun α β, α → β</code>.</p></main><nav class="nav"><iframe src="./navbar.html" class="navframe" frameBorder="0"></iframe></nav></body></html>