Skip to content

Commit 005d5b0

Browse files
github-merge-queue[bot]github-merge-queue[bot]
committed
Deploying to gh-pages from @ 3337e54 🚀
1 parent f8b7b1a commit 005d5b0

File tree

275 files changed

+2609
-2604
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

275 files changed

+2609
-2604
lines changed

‎master/Algebra.Apartness.Structures.html‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@
2323
<a id="706" class="Keyword">open</a> <a id="711" class="Keyword">import</a> <a id="718" href="Algebra.Structures.html" class="Module">Algebra.Structures</a> <a id="737" href="Algebra.Apartness.Structures.html#433" class="Bound Operator">_≈_</a> <a id="741" class="Keyword">using</a> <a id="747" class="Symbol">(</a><a id="748" href="Algebra.Structures.html#27013" class="Record">IsCommutativeRing</a><a id="765" class="Symbol">)</a>
2424
<a id="767" class="Keyword">open</a> <a id="772" class="Keyword">import</a> <a id="779" href="Relation.Binary.Structures.html" class="Module">Relation.Binary.Structures</a> <a id="806" class="Keyword">using</a> <a id="812" class="Symbol">(</a><a id="813" href="Relation.Binary.Structures.html#1595" class="Record">IsEquivalence</a><a id="826" class="Symbol">;</a> <a id="828" href="Relation.Binary.Structures.html#8699" class="Record">IsApartnessRelation</a><a id="847" class="Symbol">)</a>
2525
<a id="849" class="Keyword">open</a> <a id="854" class="Keyword">import</a> <a id="861" href="Relation.Binary.Definitions.html" class="Module">Relation.Binary.Definitions</a> <a id="889" class="Keyword">using</a> <a id="895" class="Symbol">(</a><a id="896" href="Relation.Binary.Definitions.html#3849" class="Function">Tight</a><a id="901" class="Symbol">)</a>
26-
<a id="903" class="Keyword">open</a> <a id="908" class="Keyword">import</a> <a id="915" href="Relation.Nullary.Negation.html" class="Module">Relation.Nullary.Negation</a> <a id="941" class="Keyword">using</a> <a id="947" class="Symbol">(</a><a id="948" href="Relation.Nullary.Negation.Core.html#677" class="Function Operator">¬_</a><a id="950" class="Symbol">)</a>
26+
<a id="903" class="Keyword">open</a> <a id="908" class="Keyword">import</a> <a id="915" href="Relation.Nullary.Negation.html" class="Module">Relation.Nullary.Negation</a> <a id="941" class="Keyword">using</a> <a id="947" class="Symbol">(</a><a id="948" href="Relation.Nullary.Negation.Core.html#673" class="Function Operator">¬_</a><a id="950" class="Symbol">)</a>
2727
<a id="952" class="Keyword">import</a> <a id="959" href="Relation.Binary.Properties.ApartnessRelation.html" class="Module">Relation.Binary.Properties.ApartnessRelation</a> <a id="1004" class="Symbol">as</a> <a id="1007" class="Module">AR</a>
2828

2929

‎master/Algebra.Construct.LexProduct.Base.html‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@
1212
<a id="371" class="Keyword">open</a> <a id="376" class="Keyword">import</a> <a id="383" href="Data.Product.Base.html" class="Module">Data.Product.Base</a> <a id="401" class="Keyword">using</a> <a id="407" class="Symbol">(</a><a id="408" href="Data.Product.Base.html#1618" class="Function Operator">_×_</a><a id="411" class="Symbol">;</a> <a id="413" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">_,_</a><a id="416" class="Symbol">)</a>
1313
<a id="418" class="Keyword">open</a> <a id="423" class="Keyword">import</a> <a id="430" href="Relation.Binary.Core.html" class="Module">Relation.Binary.Core</a> <a id="451" class="Keyword">using</a> <a id="457" class="Symbol">(</a><a id="458" href="Relation.Binary.Core.html#896" class="Function">Rel</a><a id="461" class="Symbol">)</a>
1414
<a id="463" class="Keyword">open</a> <a id="468" class="Keyword">import</a> <a id="475" href="Relation.Binary.Definitions.html" class="Module">Relation.Binary.Definitions</a> <a id="503" class="Keyword">using</a> <a id="509" class="Symbol">(</a><a id="510" href="Relation.Binary.Definitions.html#6907" class="Function">Decidable</a><a id="519" class="Symbol">)</a>
15-
<a id="521" class="Keyword">open</a> <a id="526" class="Keyword">import</a> <a id="533" href="Relation.Nullary.Decidable.Core.html" class="Module">Relation.Nullary.Decidable.Core</a> <a id="565" class="Keyword">using</a> <a id="571" class="Symbol">(</a><a id="572" href="Relation.Nullary.Decidable.Core.html#2032" class="Field">does</a><a id="576" class="Symbol">;</a> <a id="578" href="Relation.Nullary.Decidable.Core.html#2099" class="InductiveConstructor">yes</a><a id="581" class="Symbol">;</a> <a id="583" href="Relation.Nullary.Decidable.Core.html#2136" class="InductiveConstructor">no</a><a id="585" class="Symbol">)</a>
15+
<a id="521" class="Keyword">open</a> <a id="526" class="Keyword">import</a> <a id="533" href="Relation.Nullary.Decidable.Core.html" class="Module">Relation.Nullary.Decidable.Core</a> <a id="565" class="Keyword">using</a> <a id="571" class="Symbol">(</a><a id="572" href="Relation.Nullary.Decidable.Core.html#2038" class="Field">does</a><a id="576" class="Symbol">;</a> <a id="578" href="Relation.Nullary.Decidable.Core.html#2105" class="InductiveConstructor">yes</a><a id="581" class="Symbol">;</a> <a id="583" href="Relation.Nullary.Decidable.Core.html#2142" class="InductiveConstructor">no</a><a id="585" class="Symbol">)</a>
1616

1717
<a id="588" class="Keyword">module</a> <a id="595" href="Algebra.Construct.LexProduct.Base.html" class="Module">Algebra.Construct.LexProduct.Base</a>
1818
<a id="631" class="Symbol">{</a><a id="632" href="Algebra.Construct.LexProduct.Base.html#632" class="Bound">a</a> <a id="634" href="Algebra.Construct.LexProduct.Base.html#634" class="Bound">b</a> <a id="636" href="Algebra.Construct.LexProduct.Base.html#636" class="Bound">ℓ</a><a id="637" class="Symbol">}</a> <a id="639" class="Symbol">{</a><a id="640" href="Algebra.Construct.LexProduct.Base.html#640" class="Bound">A</a> <a id="642" class="Symbol">:</a> <a id="644" href="Agda.Primitive.html#388" class="Primitive">Set</a> <a id="648" href="Algebra.Construct.LexProduct.Base.html#632" class="Bound">a</a><a id="649" class="Symbol">}</a> <a id="651" class="Symbol">{</a><a id="652" href="Algebra.Construct.LexProduct.Base.html#652" class="Bound">B</a> <a id="654" class="Symbol">:</a> <a id="656" href="Agda.Primitive.html#388" class="Primitive">Set</a> <a id="660" href="Algebra.Construct.LexProduct.Base.html#634" class="Bound">b</a><a id="661" class="Symbol">}</a>
@@ -28,7 +28,7 @@
2828
<a id="973" class="Comment">-- operator that only calculates the second component of product.</a>
2929

3030
<a id="innerLex"></a><a id="1040" href="Algebra.Construct.LexProduct.Base.html#1040" class="Function">innerLex</a> <a id="1049" class="Symbol">:</a> <a id="1051" href="Algebra.Construct.LexProduct.Base.html#640" class="Bound">A</a> <a id="1053" class="Symbol">→</a> <a id="1055" href="Algebra.Construct.LexProduct.Base.html#640" class="Bound">A</a> <a id="1057" class="Symbol">→</a> <a id="1059" href="Algebra.Construct.LexProduct.Base.html#652" class="Bound">B</a> <a id="1061" class="Symbol">→</a> <a id="1063" href="Algebra.Construct.LexProduct.Base.html#652" class="Bound">B</a> <a id="1065" class="Symbol">→</a> <a id="1067" href="Algebra.Construct.LexProduct.Base.html#652" class="Bound">B</a>
31-
<a id="1069" href="Algebra.Construct.LexProduct.Base.html#1040" class="Function">innerLex</a> <a id="1078" href="Algebra.Construct.LexProduct.Base.html#1078" class="Bound">a</a> <a id="1080" href="Algebra.Construct.LexProduct.Base.html#1080" class="Bound">b</a> <a id="1082" href="Algebra.Construct.LexProduct.Base.html#1082" class="Bound">x</a> <a id="1084" href="Algebra.Construct.LexProduct.Base.html#1084" class="Bound">y</a> <a id="1086" class="Keyword">with</a> <a id="1091" href="Relation.Nullary.Decidable.Core.html#2032" class="Field">does</a> <a id="1096" class="Symbol">((</a><a id="1098" href="Algebra.Construct.LexProduct.Base.html#1078" class="Bound">a</a> <a id="1100" href="Algebra.Construct.LexProduct.Base.html#666" class="Bound Operator">∙</a> <a id="1102" href="Algebra.Construct.LexProduct.Base.html#1080" class="Bound">b</a><a id="1103" class="Symbol">)</a> <a id="1105" href="Algebra.Construct.LexProduct.Base.html#713" class="Bound Operator">≟₁</a> <a id="1108" href="Algebra.Construct.LexProduct.Base.html#1078" class="Bound">a</a><a id="1109" class="Symbol">)</a> <a id="1111" class="Symbol">|</a> <a id="1113" href="Relation.Nullary.Decidable.Core.html#2032" class="Field">does</a> <a id="1118" class="Symbol">((</a><a id="1120" href="Algebra.Construct.LexProduct.Base.html#1078" class="Bound">a</a> <a id="1122" href="Algebra.Construct.LexProduct.Base.html#666" class="Bound Operator">∙</a> <a id="1124" href="Algebra.Construct.LexProduct.Base.html#1080" class="Bound">b</a><a id="1125" class="Symbol">)</a> <a id="1127" href="Algebra.Construct.LexProduct.Base.html#713" class="Bound Operator">≟₁</a> <a id="1130" href="Algebra.Construct.LexProduct.Base.html#1080" class="Bound">b</a><a id="1131" class="Symbol">)</a>
31+
<a id="1069" href="Algebra.Construct.LexProduct.Base.html#1040" class="Function">innerLex</a> <a id="1078" href="Algebra.Construct.LexProduct.Base.html#1078" class="Bound">a</a> <a id="1080" href="Algebra.Construct.LexProduct.Base.html#1080" class="Bound">b</a> <a id="1082" href="Algebra.Construct.LexProduct.Base.html#1082" class="Bound">x</a> <a id="1084" href="Algebra.Construct.LexProduct.Base.html#1084" class="Bound">y</a> <a id="1086" class="Keyword">with</a> <a id="1091" href="Relation.Nullary.Decidable.Core.html#2038" class="Field">does</a> <a id="1096" class="Symbol">((</a><a id="1098" href="Algebra.Construct.LexProduct.Base.html#1078" class="Bound">a</a> <a id="1100" href="Algebra.Construct.LexProduct.Base.html#666" class="Bound Operator">∙</a> <a id="1102" href="Algebra.Construct.LexProduct.Base.html#1080" class="Bound">b</a><a id="1103" class="Symbol">)</a> <a id="1105" href="Algebra.Construct.LexProduct.Base.html#713" class="Bound Operator">≟₁</a> <a id="1108" href="Algebra.Construct.LexProduct.Base.html#1078" class="Bound">a</a><a id="1109" class="Symbol">)</a> <a id="1111" class="Symbol">|</a> <a id="1113" href="Relation.Nullary.Decidable.Core.html#2038" class="Field">does</a> <a id="1118" class="Symbol">((</a><a id="1120" href="Algebra.Construct.LexProduct.Base.html#1078" class="Bound">a</a> <a id="1122" href="Algebra.Construct.LexProduct.Base.html#666" class="Bound Operator">∙</a> <a id="1124" href="Algebra.Construct.LexProduct.Base.html#1080" class="Bound">b</a><a id="1125" class="Symbol">)</a> <a id="1127" href="Algebra.Construct.LexProduct.Base.html#713" class="Bound Operator">≟₁</a> <a id="1130" href="Algebra.Construct.LexProduct.Base.html#1080" class="Bound">b</a><a id="1131" class="Symbol">)</a>
3232
<a id="1133" class="Symbol">...</a> <a id="1137" class="Symbol">|</a> <a id="1139" href="Agda.Builtin.Bool.html#198" class="InductiveConstructor">true</a> <a id="1145" class="Symbol">|</a> <a id="1147" href="Agda.Builtin.Bool.html#192" class="InductiveConstructor">false</a> <a id="1153" class="Symbol">=</a> <a id="1155" class="Bound">x</a>
3333
<a id="1157" class="Symbol">...</a> <a id="1161" class="Symbol">|</a> <a id="1163" href="Agda.Builtin.Bool.html#192" class="InductiveConstructor">false</a> <a id="1169" class="Symbol">|</a> <a id="1171" href="Agda.Builtin.Bool.html#198" class="InductiveConstructor">true</a> <a id="1177" class="Symbol">=</a> <a id="1179" class="Bound">y</a>
3434
<a id="1181" class="CatchallClause Symbol">...</a><a id="1184" class="CatchallClause"> </a><a id="1185" class="CatchallClause Symbol">|</a><a id="1186" class="CatchallClause"> </a><a id="1191" class="CatchallClause Symbol">_</a><a id="1192" class="CatchallClause"> </a><a id="1193" class="CatchallClause Symbol">|</a><a id="1194" class="CatchallClause"> </a><a id="1199" class="CatchallClause Symbol">_</a> <a id="1201" class="Symbol">=</a> <a id="1203" class="Bound">x</a> <a id="1205" href="Algebra.Construct.LexProduct.Base.html#680" class="Bound Operator">◦</a> <a id="1207" class="Bound">y</a>

0 commit comments

Comments
 (0)