Deploying to gh-pages from @ d970b78 🚀

agda · Jun 5, 2024 · 2857149 · 2857149
1 parent 3cbef5f
commit 2857149
Show file tree

Hide file tree

Showing 15 changed files with 209 additions and 208 deletions.
diff --git a/master/Data.List.Base.html b/master/Data.List.Base.html
diff --git a/master/Data.List.Membership.Propositional.Properties.html b/master/Data.List.Membership.Propositional.Properties.html
diff --git a/master/Data.List.Membership.Setoid.Properties.html b/master/Data.List.Membership.Setoid.Properties.html
diff --git a/master/Data.List.Properties.html b/master/Data.List.Properties.html
diff --git a/master/Data.List.Relation.Binary.Subset.Setoid.Properties.html b/master/Data.List.Relation.Binary.Subset.Setoid.Properties.html
@@ -10,7 +10,7 @@
 <a id="297" class="Keyword">module</a> <a id="304" href="Data.List.Relation.Binary.Subset.Setoid.Properties.html" class="Module">Data.List.Relation.Binary.Subset.Setoid.Properties</a> <a id="355" class="Keyword">where</a>
 
 <a id="362" class="Keyword">open</a> <a id="367" class="Keyword">import</a> <a id="374" href="Data.Bool.Base.html" class="Module">Data.Bool.Base</a> <a id="389" class="Keyword">using</a> <a id="395" class="Symbol">(</a><a id="396" href="Agda.Builtin.Bool.html#173" class="Datatype">Bool</a><a id="400" class="Symbol">;</a> <a id="402" href="Agda.Builtin.Bool.html#198" class="InductiveConstructor">true</a><a id="406" class="Symbol">;</a> <a id="408" href="Agda.Builtin.Bool.html#192" class="InductiveConstructor">false</a><a id="413" class="Symbol">)</a>
-<a id="415" class="Keyword">open</a> <a id="420" class="Keyword">import</a> <a id="427" href="Data.List.Base.html" class="Module">Data.List.Base</a> <a id="442" class="Keyword">hiding</a> <a id="449" class="Symbol">(</a><a id="450" href="Data.List.Base.html#7423" class="Function Operator">_∷ʳ_</a><a id="454" class="Symbol">;</a> <a id="456" href="Data.List.Base.html#13561" class="Function">find</a><a id="460" class="Symbol">)</a>
+<a id="415" class="Keyword">open</a> <a id="420" class="Keyword">import</a> <a id="427" href="Data.List.Base.html" class="Module">Data.List.Base</a> <a id="442" class="Keyword">hiding</a> <a id="449" class="Symbol">(</a><a id="450" href="Data.List.Base.html#7423" class="Function Operator">_∷ʳ_</a><a id="454" class="Symbol">;</a> <a id="456" href="Data.List.Base.html#13535" class="Function">find</a><a id="460" class="Symbol">)</a>
 <a id="462" class="Keyword">import</a> <a id="469" href="Data.List.Properties.html" class="Module">Data.List.Properties</a> <a id="490" class="Symbol">as</a> <a id="493" class="Module">List</a>
 <a id="498" class="Keyword">open</a> <a id="503" class="Keyword">import</a> <a id="510" href="Data.List.Relation.Unary.Any.html" class="Module">Data.List.Relation.Unary.Any</a> <a id="539" class="Symbol">as</a> <a id="542" class="Module">Any</a> <a id="546" class="Keyword">using</a> <a id="552" class="Symbol">(</a><a id="553" href="Data.List.Relation.Unary.Any.html#1166" class="Datatype">Any</a><a id="556" class="Symbol">;</a> <a id="558" href="Data.List.Relation.Unary.Any.html#1229" class="InductiveConstructor">here</a><a id="562" class="Symbol">;</a> <a id="564" href="Data.List.Relation.Unary.Any.html#1282" class="InductiveConstructor">there</a><a id="569" class="Symbol">)</a>
 <a id="571" class="Keyword">open</a> <a id="576" class="Keyword">import</a> <a id="583" href="Data.List.Relation.Unary.All.html" class="Module">Data.List.Relation.Unary.All</a> <a id="612" class="Symbol">as</a> <a id="615" class="Module">All</a> <a id="619" class="Keyword">using</a> <a id="625" class="Symbol">(</a><a id="626" href="Data.List.Relation.Unary.All.html#1630" class="Datatype">All</a><a id="629" class="Symbol">)</a>

diff --git a/master/Data.List.Relation.Unary.All.Properties.html b/master/Data.List.Relation.Unary.All.Properties.html
diff --git a/master/Data.List.Relation.Unary.Any.Properties.html b/master/Data.List.Relation.Unary.Any.Properties.html
diff --git a/master/Data.List.Relation.Unary.Any.html b/master/Data.List.Relation.Unary.Any.html
@@ -66,7 +66,7 @@
 <a id="2015" class="Keyword">infixr</a> <a id="2022" class="Number">5</a> <a id="2024" href="Data.List.Relation.Unary.Any.html#2030" class="Function Operator">_∷=_</a>
 
 <a id="_∷=_"></a><a id="2030" href="Data.List.Relation.Unary.Any.html#2030" class="Function Operator">_∷=_</a> <a id="2035" class="Symbol">:</a> <a id="2037" class="Symbol">{</a><a id="2038" href="Data.List.Relation.Unary.Any.html#2038" class="Bound">P</a> <a id="2040" class="Symbol">:</a> <a id="2042" href="Relation.Unary.html#1229" class="Function">Pred</a> <a id="2047" href="Data.List.Relation.Unary.Any.html#866" class="Generalizable">A</a> <a id="2049" href="Data.List.Relation.Unary.Any.html#850" class="Generalizable">p</a><a id="2050" class="Symbol">}</a> <a id="2052" class="Symbol">→</a> <a id="2054" href="Data.List.Relation.Unary.Any.html#1166" class="Datatype">Any</a> <a id="2058" href="Data.List.Relation.Unary.Any.html#2038" class="Bound">P</a> <a id="2060" href="Data.List.Relation.Unary.Any.html#909" class="Generalizable">xs</a> <a id="2063" class="Symbol">→</a> <a id="2065" href="Data.List.Relation.Unary.Any.html#866" class="Generalizable">A</a> <a id="2067" class="Symbol">→</a> <a id="2069" href="Agda.Builtin.List.html#147" class="Datatype">List</a> <a id="2074" href="Data.List.Relation.Unary.Any.html#866" class="Generalizable">A</a>
-<a id="2076" href="Data.List.Relation.Unary.Any.html#2030" class="Function Operator">_∷=_</a> <a id="2081" class="Symbol">{</a><a id="2082" class="Argument">xs</a> <a id="2085" class="Symbol">=</a> <a id="2087" href="Data.List.Relation.Unary.Any.html#2087" class="Bound">xs</a><a id="2089" class="Symbol">}</a> <a id="2091" href="Data.List.Relation.Unary.Any.html#2091" class="Bound">x∈xs</a> <a id="2096" href="Data.List.Relation.Unary.Any.html#2096" class="Bound">v</a> <a id="2098" class="Symbol">=</a> <a id="2100" href="Data.List.Relation.Unary.Any.html#2087" class="Bound">xs</a> <a id="2103" href="Data.List.Base.html#14916" class="Function Operator">List.[</a> <a id="2110" href="Data.List.Relation.Unary.Any.html#1827" class="Function">index</a> <a id="2116" href="Data.List.Relation.Unary.Any.html#2091" class="Bound">x∈xs</a> <a id="2121" href="Data.List.Base.html#14916" class="Function Operator">]∷=</a> <a id="2125" href="Data.List.Relation.Unary.Any.html#2096" class="Bound">v</a>
+<a id="2076" href="Data.List.Relation.Unary.Any.html#2030" class="Function Operator">_∷=_</a> <a id="2081" class="Symbol">{</a><a id="2082" class="Argument">xs</a> <a id="2085" class="Symbol">=</a> <a id="2087" href="Data.List.Relation.Unary.Any.html#2087" class="Bound">xs</a><a id="2089" class="Symbol">}</a> <a id="2091" href="Data.List.Relation.Unary.Any.html#2091" class="Bound">x∈xs</a> <a id="2096" href="Data.List.Relation.Unary.Any.html#2096" class="Bound">v</a> <a id="2098" class="Symbol">=</a> <a id="2100" href="Data.List.Relation.Unary.Any.html#2087" class="Bound">xs</a> <a id="2103" href="Data.List.Base.html#14890" class="Function Operator">List.[</a> <a id="2110" href="Data.List.Relation.Unary.Any.html#1827" class="Function">index</a> <a id="2116" href="Data.List.Relation.Unary.Any.html#2091" class="Bound">x∈xs</a> <a id="2121" href="Data.List.Base.html#14890" class="Function Operator">]∷=</a> <a id="2125" href="Data.List.Relation.Unary.Any.html#2096" class="Bound">v</a>
 
 <a id="2128" class="Keyword">infixl</a> <a id="2135" class="Number">4</a> <a id="2137" href="Data.List.Relation.Unary.Any.html#2141" class="Function Operator">_─_</a>
 <a id="_─_"></a><a id="2141" href="Data.List.Relation.Unary.Any.html#2141" class="Function Operator">_─_</a> <a id="2145" class="Symbol">:</a> <a id="2147" class="Symbol">{</a><a id="2148" href="Data.List.Relation.Unary.Any.html#2148" class="Bound">P</a> <a id="2150" class="Symbol">:</a> <a id="2152" href="Relation.Unary.html#1229" class="Function">Pred</a> <a id="2157" href="Data.List.Relation.Unary.Any.html#866" class="Generalizable">A</a> <a id="2159" href="Data.List.Relation.Unary.Any.html#850" class="Generalizable">p</a><a id="2160" class="Symbol">}</a> <a id="2162" class="Symbol">→</a> <a id="2164" class="Symbol">∀</a> <a id="2166" href="Data.List.Relation.Unary.Any.html#2166" class="Bound">xs</a> <a id="2169" class="Symbol">→</a> <a id="2171" href="Data.List.Relation.Unary.Any.html#1166" class="Datatype">Any</a> <a id="2175" href="Data.List.Relation.Unary.Any.html#2148" class="Bound">P</a> <a id="2177" href="Data.List.Relation.Unary.Any.html#2166" class="Bound">xs</a> <a id="2180" class="Symbol">→</a> <a id="2182" href="Agda.Builtin.List.html#147" class="Datatype">List</a> <a id="2187" href="Data.List.Relation.Unary.Any.html#866" class="Generalizable">A</a>

diff --git a/master/Data.List.Relation.Unary.Enumerates.Setoid.Properties.html b/master/Data.List.Relation.Unary.Enumerates.Setoid.Properties.html
@@ -78,7 +78,7 @@
   <a id="2887" class="Keyword">open</a> <a id="2892" href="Relation.Binary.Bundles.html#1563" class="Module">DecSetoid</a> <a id="2902" href="Data.List.Relation.Unary.Enumerates.Setoid.Properties.html#2858" class="Bound">S?</a> <a id="2905" class="Keyword">renaming</a> <a id="2914" class="Symbol">(</a><a id="2915" href="Relation.Binary.Bundles.html#1818" class="Function">setoid</a> <a id="2922" class="Symbol">to</a> <a id="2925" class="Function">S</a><a id="2926" class="Symbol">)</a>
 
   <a id="2931" href="Data.List.Relation.Unary.Enumerates.Setoid.Properties.html#2931" class="Function">deduplicate⁺</a> <a id="2944" class="Symbol">:</a> <a id="2946" class="Symbol">∀</a> <a id="2948" class="Symbol">{</a><a id="2949" href="Data.List.Relation.Unary.Enumerates.Setoid.Properties.html#2949" class="Bound">xs</a><a id="2951" class="Symbol">}</a> <a id="2953" class="Symbol">→</a> <a id="2955" href="Data.List.Relation.Unary.Enumerates.Setoid.html#639" class="Function">IsEnumeration</a> <a id="2969" href="Data.List.Relation.Unary.Enumerates.Setoid.Properties.html#2925" class="Function">S</a> <a id="2971" href="Data.List.Relation.Unary.Enumerates.Setoid.Properties.html#2949" class="Bound">xs</a> <a id="2974" class="Symbol">→</a>
-                 <a id="2993" href="Data.List.Relation.Unary.Enumerates.Setoid.html#639" class="Function">IsEnumeration</a> <a id="3007" href="Data.List.Relation.Unary.Enumerates.Setoid.Properties.html#2925" class="Function">S</a> <a id="3009" class="Symbol">(</a><a id="3010" href="Data.List.Base.html#13256" class="Function">deduplicate</a> <a id="3022" href="Relation.Binary.Structures.html#1949" class="Function Operator">_≟_</a> <a id="3026" href="Data.List.Relation.Unary.Enumerates.Setoid.Properties.html#2949" class="Bound">xs</a><a id="3028" class="Symbol">)</a>
+                 <a id="2993" href="Data.List.Relation.Unary.Enumerates.Setoid.html#639" class="Function">IsEnumeration</a> <a id="3007" href="Data.List.Relation.Unary.Enumerates.Setoid.Properties.html#2925" class="Function">S</a> <a id="3009" class="Symbol">(</a><a id="3010" href="Data.List.Base.html#13230" class="Function">deduplicate</a> <a id="3022" href="Relation.Binary.Structures.html#1949" class="Function Operator">_≟_</a> <a id="3026" href="Data.List.Relation.Unary.Enumerates.Setoid.Properties.html#2949" class="Bound">xs</a><a id="3028" class="Symbol">)</a>
   <a id="3032" href="Data.List.Relation.Unary.Enumerates.Setoid.Properties.html#2931" class="Function">deduplicate⁺</a> <a id="3045" class="Symbol">=</a> <a id="3047" href="Data.List.Membership.Setoid.Properties.html#13535" class="Function">∈-deduplicate⁺</a> <a id="3062" href="Data.List.Relation.Unary.Enumerates.Setoid.Properties.html#2925" class="Function">S</a> <a id="3064" href="Relation.Binary.Structures.html#1949" class="Function Operator">_≟_</a> <a id="3068" class="Symbol">(</a><a id="3069" href="Relation.Binary.Properties.Setoid.html#2611" class="Function">respʳ-flip</a> <a id="3080" href="Data.List.Relation.Unary.Enumerates.Setoid.Properties.html#2925" class="Function">S</a><a id="3081" class="Symbol">)</a> <a id="3083" href="Function.Base.html#1115" class="Function Operator">∘_</a>
 
 <a id="3087" class="Comment">------------------------------------------------------------------------</a>