Deploying to web from @ b270472 🚀

plfa · Oct 11, 2024 · 3c682cb · 3c682cb
1 parent fb01618
commit 3c682cb
Show file tree

Hide file tree

Showing 16 changed files with 2,428 additions and 2,428 deletions.
diff --git a/Connectives/index.html b/Connectives/index.html
diff --git a/Decidable/index.html b/Decidable/index.html
diff --git a/Induction/index.html b/Induction/index.html
diff --git a/Lists/index.html b/Lists/index.html
diff --git a/Negation/index.html b/Negation/index.html
diff --git a/Quantifiers/index.html b/Quantifiers/index.html
diff --git a/Relations/index.html b/Relations/index.html
@@ -214,9 +214,9 @@
 1 ≤ n
 ---------------------
 to (2 * n) ≡ (to n) O</code></pre><pre class="Agda"><a id="plfa_plfa-part1-Relations-25894" class="Comment">-- Your code goes here</a>
-</pre><h2 id="standard-library">Standard library</h2>Definitions similar to those in this chapter can be found in the standard library:<pre class="Agda"><a id="plfa_plfa-part1-Relations-26034" class="Keyword">import</a> <a id="plfa_plfa-part1-Relations-26041" href="https://agda.github.io/agda-stdlib/v2.1/Data.Nat.html" class="Module">Data.Nat</a> <a id="plfa_plfa-part1-Relations-26050" class="Keyword">using</a> <a id="plfa_plfa-part1-Relations-26056" class="Symbol">(</a><a id="plfa_plfa-part1-Relations-26057" href="https://agda.github.io/agda-stdlib/v2.1/Data.Nat.Base.html#1691" class="Datatype Operator">_≤_</a><a id="plfa_plfa-part1-Relations-26060" class="Symbol">;</a> <a id="plfa_plfa-part1-Relations-26062" href="https://agda.github.io/agda-stdlib/v2.1/Data.Nat.Base.html#1714" class="InductiveConstructor">z≤n</a><a id="plfa_plfa-part1-Relations-26065" class="Symbol">;</a> <a id="plfa_plfa-part1-Relations-26067" href="https://agda.github.io/agda-stdlib/v2.1/Data.Nat.Base.html#1756" class="InductiveConstructor">s≤s</a><a id="plfa_plfa-part1-Relations-26070" class="Symbol">)</a>
-<a id="plfa_plfa-part1-Relations-26072" class="Keyword">import</a> <a id="plfa_plfa-part1-Relations-26079" href="https://agda.github.io/agda-stdlib/v2.1/Data.Nat.Properties.html" class="Module">Data.Nat.Properties</a> <a id="plfa_plfa-part1-Relations-26099" class="Keyword">using</a> <a id="plfa_plfa-part1-Relations-26105" class="Symbol">(</a><a id="plfa_plfa-part1-Relations-26106" href="https://agda.github.io/agda-stdlib/v2.1/Data.Nat.Properties.html#5805" class="Function">≤-refl</a><a id="plfa_plfa-part1-Relations-26112" class="Symbol">;</a> <a id="plfa_plfa-part1-Relations-26114" href="https://agda.github.io/agda-stdlib/v2.1/Data.Nat.Properties.html#5988" class="Function">≤-trans</a><a id="plfa_plfa-part1-Relations-26121" class="Symbol">;</a> <a id="plfa_plfa-part1-Relations-26123" href="https://agda.github.io/agda-stdlib/v2.1/Data.Nat.Properties.html#5855" class="Function">≤-antisym</a><a id="plfa_plfa-part1-Relations-26132" class="Symbol">;</a> <a id="plfa_plfa-part1-Relations-26134" href="https://agda.github.io/agda-stdlib/v2.1/Data.Nat.Properties.html#6100" class="Function">≤-total</a><a id="plfa_plfa-part1-Relations-26141" class="Symbol">;</a>
-                                  <a id="plfa_plfa-part1-Relations-26177" href="https://agda.github.io/agda-stdlib/v2.1/Data.Nat.Properties.html#19646" class="Function">+-monoʳ-≤</a><a id="plfa_plfa-part1-Relations-26186" class="Symbol">;</a> <a id="plfa_plfa-part1-Relations-26188" href="https://agda.github.io/agda-stdlib/v2.1/Data.Nat.Properties.html#19556" class="Function">+-monoˡ-≤</a><a id="plfa_plfa-part1-Relations-26197" class="Symbol">;</a> <a id="plfa_plfa-part1-Relations-26199" href="https://agda.github.io/agda-stdlib/v2.1/Data.Nat.Properties.html#19400" class="Function">+-mono-≤</a><a id="plfa_plfa-part1-Relations-26207" class="Symbol">)</a>
+</pre><h2 id="standard-library">Standard library</h2>Definitions similar to those in this chapter can be found in the standard library:<pre class="Agda"><a id="plfa_plfa-part1-Relations-26034" class="Keyword">import</a> <a id="plfa_plfa-part1-Relations-26041" href="https://agda.github.io/agda-stdlib/v2.1/Data.Nat.html" class="Module">Data.Nat</a> <a id="plfa_plfa-part1-Relations-26050" class="Keyword">using</a> <a id="plfa_plfa-part1-Relations-26056" class="Symbol">(</a><a id="plfa_plfa-part1-Relations-26057" href="https://agda.github.io/agda-stdlib/v2.1/Data.Nat.Base.html#1691" class="Datatype Operator">_≤_</a><a id="plfa_plfa-part1-Relations-26060" class="Symbol">;</a> <a id="plfa_plfa-part1-Relations-26062" href="https://agda.github.io/agda-stdlib/v2.1/Data.Nat.Base.html#1714" class="InductiveConstructor">z≤n</a><a id="plfa_plfa-part1-Relations-26065" class="Symbol">;</a> <a id="plfa_plfa-part1-Relations-26067" href="https://agda.github.io/agda-stdlib/v2.1/Data.Nat.Base.html#1756" class="InductiveConstructor">s≤s</a><a id="plfa_plfa-part1-Relations-26070" class="Symbol">;</a> <a id="plfa_plfa-part1-Relations-26072" href="https://agda.github.io/agda-stdlib/v2.1/Data.Nat.Base.html#1801" class="Function Operator">_&lt;_</a><a id="plfa_plfa-part1-Relations-26075" class="Symbol">)</a>
+<a id="plfa_plfa-part1-Relations-26077" class="Keyword">import</a> <a id="plfa_plfa-part1-Relations-26084" href="https://agda.github.io/agda-stdlib/v2.1/Data.Nat.Properties.html" class="Module">Data.Nat.Properties</a> <a id="plfa_plfa-part1-Relations-26104" class="Keyword">using</a> <a id="plfa_plfa-part1-Relations-26110" class="Symbol">(</a><a id="plfa_plfa-part1-Relations-26111" href="https://agda.github.io/agda-stdlib/v2.1/Data.Nat.Properties.html#5805" class="Function">≤-refl</a><a id="plfa_plfa-part1-Relations-26117" class="Symbol">;</a> <a id="plfa_plfa-part1-Relations-26119" href="https://agda.github.io/agda-stdlib/v2.1/Data.Nat.Properties.html#5988" class="Function">≤-trans</a><a id="plfa_plfa-part1-Relations-26126" class="Symbol">;</a> <a id="plfa_plfa-part1-Relations-26128" href="https://agda.github.io/agda-stdlib/v2.1/Data.Nat.Properties.html#5855" class="Function">≤-antisym</a><a id="plfa_plfa-part1-Relations-26137" class="Symbol">;</a> <a id="plfa_plfa-part1-Relations-26139" href="https://agda.github.io/agda-stdlib/v2.1/Data.Nat.Properties.html#6100" class="Function">≤-total</a><a id="plfa_plfa-part1-Relations-26146" class="Symbol">;</a>
+                                  <a id="plfa_plfa-part1-Relations-26182" href="https://agda.github.io/agda-stdlib/v2.1/Data.Nat.Properties.html#19646" class="Function">+-monoʳ-≤</a><a id="plfa_plfa-part1-Relations-26191" class="Symbol">;</a> <a id="plfa_plfa-part1-Relations-26193" href="https://agda.github.io/agda-stdlib/v2.1/Data.Nat.Properties.html#19556" class="Function">+-monoˡ-≤</a><a id="plfa_plfa-part1-Relations-26202" class="Symbol">;</a> <a id="plfa_plfa-part1-Relations-26204" href="https://agda.github.io/agda-stdlib/v2.1/Data.Nat.Properties.html#19400" class="Function">+-mono-≤</a><a id="plfa_plfa-part1-Relations-26212" class="Symbol">)</a>
 </pre><p>In the standard library, <code>≤-total</code> is formalised in terms of disjunction (which we define in Chapter <a href="../Connectives/">Connectives</a>), and <code>+-monoʳ-≤</code>, <code>+-monoˡ-≤</code>, <code>+-mono-≤</code> are proved differently than here, and more arguments are implicit.</p><h2 id="unicode">Unicode</h2><p>This chapter uses the following unicode:</p><pre><code>≤  U+2264  LESS-THAN OR EQUAL TO (\&lt;=, \le)
 ≥  U+2265  GREATER-THAN OR EQUAL TO (\&gt;=, \ge)
 ˡ  U+02E1  MODIFIER LETTER SMALL L (\^l)