Skip to content

Commit

Permalink
Deploying to gh-pages from @ cc69ea0 🚀
Browse files Browse the repository at this point in the history
  • Loading branch information
@github-merge-queue
github-merge-queue[bot] committed Aug 30, 2024
1 parent 04e336a commit fc6cf30
Show file tree
Hide file tree
Showing 13 changed files with 141 additions and 141 deletions.
10 changes: 5 additions & 5 deletions master/Data.List.Extrema.html
View file

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion master/Data.List.Membership.Setoid.Properties.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -83,7 +83,7 @@

<a id="3046" class="Keyword">private</a>
<a id="3058" href="Data.List.Membership.Setoid.Properties.html#3058" class="Function">∉×∈⇒≉</a> <a id="3064" class="Symbol">:</a> <a id="3066" class="Symbol">∀</a> <a id="3068" class="Symbol">{</a><a id="3069" href="Data.List.Membership.Setoid.Properties.html#3069" class="Bound">x</a> <a id="3071" href="Data.List.Membership.Setoid.Properties.html#3071" class="Bound">y</a> <a id="3073" href="Data.List.Membership.Setoid.Properties.html#3073" class="Bound">xs</a><a id="3075" class="Symbol">}</a> <a id="3077" class="Symbol">→</a> <a id="3079" href="Data.List.Relation.Unary.All.html#1644" class="Datatype">All</a> <a id="3083" class="Symbol">(</a><a id="3084" href="Data.List.Membership.Setoid.Properties.html#3071" class="Bound">y</a> <a id="3086" href="Relation.Binary.Bundles.html#1046" class="Function Operator">≉_</a><a id="3088" class="Symbol">)</a> <a id="3090" href="Data.List.Membership.Setoid.Properties.html#3073" class="Bound">xs</a> <a id="3093" class="Symbol">→</a> <a id="3095" href="Data.List.Membership.Setoid.Properties.html#3069" class="Bound">x</a> <a id="3097" href="Data.List.Membership.Setoid.html#925" class="Function Operator">∈</a> <a id="3099" href="Data.List.Membership.Setoid.Properties.html#3073" class="Bound">xs</a> <a id="3102" class="Symbol">→</a> <a id="3104" href="Data.List.Membership.Setoid.Properties.html#3069" class="Bound">x</a> <a id="3106" href="Relation.Binary.Bundles.html#1046" class="Function Operator">≉</a> <a id="3108" href="Data.List.Membership.Setoid.Properties.html#3071" class="Bound">y</a>
<a id="3114" href="Data.List.Membership.Setoid.Properties.html#3058" class="Function">∉×∈⇒≉</a> <a id="3120" class="Symbol">=</a> <a id="3122" href="Data.List.Relation.Unary.All.html#5815" class="Function">All.lookupWith</a> <a id="3137" class="Symbol">λ</a> <a id="3139" href="Data.List.Membership.Setoid.Properties.html#3139" class="Bound">y≉z</a> <a id="3143" href="Data.List.Membership.Setoid.Properties.html#3143" class="Bound">x≈z</a> <a id="3147" href="Data.List.Membership.Setoid.Properties.html#3147" class="Bound">x≈y</a> <a id="3151" class="Symbol">→</a> <a id="3153" href="Data.List.Membership.Setoid.Properties.html#3139" class="Bound">y≉z</a> <a id="3157" class="Symbol">(</a><a id="3158" href="Relation.Binary.Structures.html#1226" class="Function">trans</a> <a id="3164" class="Symbol">(</a><a id="3165" href="Relation.Binary.Structures.html#1200" class="Function">sym</a> <a id="3169" href="Data.List.Membership.Setoid.Properties.html#3147" class="Bound">x≈y</a><a id="3172" class="Symbol">)</a> <a id="3174" href="Data.List.Membership.Setoid.Properties.html#3143" class="Bound">x≈z</a><a id="3177" class="Symbol">)</a>
<a id="3114" href="Data.List.Membership.Setoid.Properties.html#3058" class="Function">∉×∈⇒≉</a> <a id="3120" class="Symbol">=</a> <a id="3122" href="Data.List.Relation.Unary.All.html#5816" class="Function">All.lookupWith</a> <a id="3137" class="Symbol">λ</a> <a id="3139" href="Data.List.Membership.Setoid.Properties.html#3139" class="Bound">y≉z</a> <a id="3143" href="Data.List.Membership.Setoid.Properties.html#3143" class="Bound">x≈z</a> <a id="3147" href="Data.List.Membership.Setoid.Properties.html#3147" class="Bound">x≈y</a> <a id="3151" class="Symbol">→</a> <a id="3153" href="Data.List.Membership.Setoid.Properties.html#3139" class="Bound">y≉z</a> <a id="3157" class="Symbol">(</a><a id="3158" href="Relation.Binary.Structures.html#1226" class="Function">trans</a> <a id="3164" class="Symbol">(</a><a id="3165" href="Relation.Binary.Structures.html#1200" class="Function">sym</a> <a id="3169" href="Data.List.Membership.Setoid.Properties.html#3147" class="Bound">x≈y</a><a id="3172" class="Symbol">)</a> <a id="3174" href="Data.List.Membership.Setoid.Properties.html#3143" class="Bound">x≈z</a><a id="3177" class="Symbol">)</a>

<a id="3182" href="Data.List.Membership.Setoid.Properties.html#3182" class="Function">unique⇒irrelevant</a> <a id="3200" class="Symbol">:</a> <a id="3202" href="Relation.Binary.Definitions.html#6066" class="Function">Binary.Irrelevant</a> <a id="3220" href="Relation.Binary.Bundles.html#1184" class="Field Operator">_≈_</a> <a id="3224" class="Symbol">→</a> <a id="3226" class="Symbol">∀</a> <a id="3228" class="Symbol">{</a><a id="3229" href="Data.List.Membership.Setoid.Properties.html#3229" class="Bound">xs</a><a id="3231" class="Symbol">}</a> <a id="3233" class="Symbol">→</a> <a id="3235" href="Data.List.Relation.Unary.Unique.Setoid.html#785" class="Datatype">Unique</a> <a id="3242" href="Data.List.Membership.Setoid.Properties.html#3229" class="Bound">xs</a> <a id="3245" class="Symbol">→</a> <a id="3247" href="Relation.Unary.html#3969" class="Function">Unary.Irrelevant</a> <a id="3264" class="Symbol">(</a><a id="3265" href="Data.List.Membership.Setoid.html#925" class="Function Operator">_∈</a> <a id="3268" href="Data.List.Membership.Setoid.Properties.html#3229" class="Bound">xs</a><a id="3270" class="Symbol">)</a>
<a id="3274" href="Data.List.Membership.Setoid.Properties.html#3182" class="Function">unique⇒irrelevant</a> <a id="3292" href="Data.List.Membership.Setoid.Properties.html#3292" class="Bound">≈-irr</a> <a id="3298" class="Symbol">_</a> <a id="3307" class="Symbol">(</a><a id="3308" href="Data.List.Relation.Unary.Any.html#1211" class="InductiveConstructor">here</a> <a id="3313" href="Data.List.Membership.Setoid.Properties.html#3313" class="Bound">p</a><a id="3314" class="Symbol">)</a> <a id="3317" class="Symbol">(</a><a id="3318" href="Data.List.Relation.Unary.Any.html#1211" class="InductiveConstructor">here</a> <a id="3323" href="Data.List.Membership.Setoid.Properties.html#3323" class="Bound">q</a><a id="3324" class="Symbol">)</a> <a id="3327" class="Symbol">=</a>
Expand Down
6 changes: 3 additions & 3 deletions master/Data.List.Relation.Binary.Disjoint.DecSetoid.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@

<a id="428" class="Keyword">open</a> <a id="433" class="Keyword">import</a> <a id="440" href="Data.Product.Base.html" class="Module">Data.Product.Base</a> <a id="458" class="Keyword">using</a> <a id="464" class="Symbol">(</a><a id="465" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">_,_</a><a id="468" class="Symbol">)</a>
<a id="470" class="Keyword">open</a> <a id="475" class="Keyword">import</a> <a id="482" href="Data.List.Relation.Unary.Any.html" class="Module">Data.List.Relation.Unary.Any</a> <a id="511" class="Keyword">using</a> <a id="517" class="Symbol">(</a><a id="518" href="Data.List.Relation.Unary.Any.html#1640" class="Function">map</a><a id="521" class="Symbol">)</a>
<a id="523" class="Keyword">open</a> <a id="528" class="Keyword">import</a> <a id="535" href="Data.List.Relation.Unary.All.html" class="Module">Data.List.Relation.Unary.All</a> <a id="564" class="Keyword">using</a> <a id="570" class="Symbol">(</a><a id="571" href="Data.List.Relation.Unary.All.html#6424" class="Function">all?</a><a id="575" class="Symbol">;</a> <a id="577" href="Data.List.Relation.Unary.All.html#6174" class="Function">lookupₛ</a><a id="584" class="Symbol">)</a>
<a id="523" class="Keyword">open</a> <a id="528" class="Keyword">import</a> <a id="535" href="Data.List.Relation.Unary.All.html" class="Module">Data.List.Relation.Unary.All</a> <a id="564" class="Keyword">using</a> <a id="570" class="Symbol">(</a><a id="571" href="Data.List.Relation.Unary.All.html#6425" class="Function">all?</a><a id="575" class="Symbol">;</a> <a id="577" href="Data.List.Relation.Unary.All.html#6175" class="Function">lookupₛ</a><a id="584" class="Symbol">)</a>
<a id="586" class="Keyword">open</a> <a id="591" class="Keyword">import</a> <a id="598" href="Data.List.Relation.Unary.All.Properties.html" class="Module">Data.List.Relation.Unary.All.Properties</a> <a id="638" class="Keyword">using</a> <a id="644" class="Symbol">(</a><a id="645" href="Data.List.Relation.Unary.All.Properties.html#3790" class="Function">¬All⇒Any¬</a><a id="654" class="Symbol">)</a>
<a id="656" class="Keyword">open</a> <a id="661" class="Keyword">import</a> <a id="668" href="Relation.Binary.Definitions.html" class="Module">Relation.Binary.Definitions</a> <a id="696" class="Keyword">using</a> <a id="702" class="Symbol">(</a><a id="703" href="Relation.Binary.Definitions.html#6713" class="Function">Decidable</a><a id="712" class="Symbol">)</a>
<a id="714" class="Keyword">open</a> <a id="719" class="Keyword">import</a> <a id="726" href="Relation.Nullary.html" class="Module">Relation.Nullary</a> <a id="743" class="Keyword">using</a> <a id="749" class="Symbol">(</a><a id="750" href="Relation.Nullary.Decidable.Core.html#1994" class="InductiveConstructor">yes</a><a id="753" class="Symbol">;</a> <a id="755" href="Relation.Nullary.Decidable.Core.html#2031" class="InductiveConstructor">no</a><a id="757" class="Symbol">;</a> <a id="759" href="Relation.Nullary.Decidable.Core.html#6289" class="Function">decidable-stable</a><a id="775" class="Symbol">)</a>
Expand All @@ -23,9 +23,9 @@
<a id="921" class="Keyword">open</a> <a id="926" class="Keyword">import</a> <a id="933" href="Data.List.Membership.DecSetoid.html" class="Module">Data.List.Membership.DecSetoid</a> <a id="964" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#402" class="Bound">S</a>

<a id="disjoint?"></a><a id="967" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#967" class="Function">disjoint?</a> <a id="977" class="Symbol">:</a> <a id="979" href="Relation.Binary.Definitions.html#6713" class="Function">Decidable</a> <a id="989" href="Data.List.Relation.Binary.Disjoint.Setoid.html#933" class="Function">Disjoint</a>
<a id="998" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#967" class="Function">disjoint?</a> <a id="1008" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#1008" class="Bound">xs</a> <a id="1011" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#1011" class="Bound">ys</a> <a id="1014" class="Keyword">with</a> <a id="1019" href="Data.List.Relation.Unary.All.html#6424" class="Function">all?</a> <a id="1024" class="Symbol">(</a><a id="1025" href="Data.List.Membership.DecSetoid.html#930" class="Function Operator">_∉?</a> <a id="1029" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#1011" class="Bound">ys</a><a id="1031" class="Symbol">)</a> <a id="1033" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#1008" class="Bound">xs</a>
<a id="998" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#967" class="Function">disjoint?</a> <a id="1008" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#1008" class="Bound">xs</a> <a id="1011" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#1011" class="Bound">ys</a> <a id="1014" class="Keyword">with</a> <a id="1019" href="Data.List.Relation.Unary.All.html#6425" class="Function">all?</a> <a id="1024" class="Symbol">(</a><a id="1025" href="Data.List.Membership.DecSetoid.html#930" class="Function Operator">_∉?</a> <a id="1029" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#1011" class="Bound">ys</a><a id="1031" class="Symbol">)</a> <a id="1033" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#1008" class="Bound">xs</a>
<a id="1036" class="Symbol">...</a> <a id="1040" class="Symbol">|</a> <a id="1042" href="Relation.Nullary.Decidable.Core.html#1994" class="InductiveConstructor">yes</a> <a id="1046" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#1046" class="Bound">xs♯ys</a> <a id="1052" class="Symbol">=</a> <a id="1054" href="Relation.Nullary.Decidable.Core.html#1994" class="InductiveConstructor">yes</a> <a id="1058" class="Symbol">λ</a> <a id="1060" class="Symbol">(</a><a id="1061" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#1061" class="Bound">v∈</a> <a id="1064" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="1066" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#1066" class="Bound">v∈′</a><a id="1069" class="Symbol">)</a> <a id="1071" class="Symbol">→</a>
<a id="1075" href="Data.List.Relation.Unary.All.html#6174" class="Function">lookupₛ</a> <a id="1083" href="Relation.Binary.Bundles.html#1818" class="Function">setoid</a> <a id="1090" class="Symbol">(λ</a> <a id="1093" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#1093" class="Bound">x≈y</a> <a id="1097" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#1097" class="Bound">∉ys</a> <a id="1101" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#1101" class="Bound">∈ys</a> <a id="1105" class="Symbol">→</a> <a id="1107" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#1097" class="Bound">∉ys</a> <a id="1111" class="Symbol">(</a><a id="1112" href="Data.List.Relation.Unary.Any.html#1640" class="Function">map</a> <a id="1116" class="Symbol">(</a><a id="1117" href="Relation.Binary.Structures.html#1226" class="Function">trans</a> <a id="1123" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#1093" class="Bound">x≈y</a><a id="1126" class="Symbol">)</a> <a id="1128" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#1101" class="Bound">∈ys</a><a id="1131" class="Symbol">))</a> <a id="1134" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#1046" class="Bound">xs♯ys</a> <a id="1140" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#1061" class="Bound">v∈</a> <a id="1143" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#1066" class="Bound">v∈′</a>
<a id="1075" href="Data.List.Relation.Unary.All.html#6175" class="Function">lookupₛ</a> <a id="1083" href="Relation.Binary.Bundles.html#1818" class="Function">setoid</a> <a id="1090" class="Symbol">(λ</a> <a id="1093" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#1093" class="Bound">x≈y</a> <a id="1097" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#1097" class="Bound">∉ys</a> <a id="1101" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#1101" class="Bound">∈ys</a> <a id="1105" class="Symbol">→</a> <a id="1107" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#1097" class="Bound">∉ys</a> <a id="1111" class="Symbol">(</a><a id="1112" href="Data.List.Relation.Unary.Any.html#1640" class="Function">map</a> <a id="1116" class="Symbol">(</a><a id="1117" href="Relation.Binary.Structures.html#1226" class="Function">trans</a> <a id="1123" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#1093" class="Bound">x≈y</a><a id="1126" class="Symbol">)</a> <a id="1128" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#1101" class="Bound">∈ys</a><a id="1131" class="Symbol">))</a> <a id="1134" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#1046" class="Bound">xs♯ys</a> <a id="1140" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#1061" class="Bound">v∈</a> <a id="1143" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#1066" class="Bound">v∈′</a>
<a id="1147" class="Symbol">...</a> <a id="1151" class="Symbol">|</a> <a id="1153" href="Relation.Nullary.Decidable.Core.html#2031" class="InductiveConstructor">no</a> <a id="1156" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#1156" class="Bound">¬xs♯ys</a> <a id="1163" class="Symbol">=</a> <a id="1165" class="Keyword">let</a> <a id="1169" class="Symbol">(</a><a id="1170" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#1170" class="Bound">x</a> <a id="1172" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="1174" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#1174" class="Bound">x∈</a> <a id="1177" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="1179" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#1179" class="Bound">¬∉ys</a><a id="1183" class="Symbol">)</a> <a id="1185" class="Symbol">=</a> <a id="1187" href="Data.List.Membership.Setoid.html#1470" class="Function">find</a> <a id="1192" class="Symbol">(</a><a id="1193" href="Data.List.Relation.Unary.All.Properties.html#3790" class="Function">¬All⇒Any¬</a> <a id="1203" class="Symbol">(</a><a id="1204" href="Data.List.Membership.DecSetoid.html#930" class="Function Operator">_∉?</a> <a id="1208" class="Symbol">_)</a> <a id="1211" class="Symbol">_</a> <a id="1213" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#1156" class="Bound">¬xs♯ys</a><a id="1219" class="Symbol">)</a> <a id="1221" class="Keyword">in</a>
<a id="1226" href="Relation.Nullary.Decidable.Core.html#2031" class="InductiveConstructor">no</a> <a id="1229" class="Symbol">λ</a> <a id="1231" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#1231" class="Bound">p</a> <a id="1233" class="Symbol">→</a> <a id="1235" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#1231" class="Bound">p</a> <a id="1237" class="Symbol">(</a><a id="1238" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#1174" class="Bound">x∈</a> <a id="1241" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="1243" href="Relation.Nullary.Decidable.Core.html#6289" class="Function">decidable-stable</a> <a id="1260" class="Symbol">(_</a> <a id="1263" href="Data.List.Membership.DecSetoid.html#883" class="Function Operator">∈?</a> <a id="1266" class="Symbol">_)</a> <a id="1269" href="Data.List.Relation.Binary.Disjoint.DecSetoid.html#1179" class="Bound">¬∉ys</a><a id="1273" class="Symbol">)</a>
</pre></body></html>
Loading

0 comments on commit fc6cf30

Please sign in to comment.