Skip to content

Commit

Permalink
Deploying to gh-pages from @ f443f9d 🚀
Browse files Browse the repository at this point in the history
  • Loading branch information
@github-merge-queue
github-merge-queue[bot] committed Mar 16, 2024
1 parent 0dd73e7 commit 0c269d9
Show file tree
Hide file tree
Showing 12 changed files with 3,619 additions and 3,369 deletions.
12 changes: 6 additions & 6 deletions master/Data.List.Relation.Binary.BagAndSetEquality.html
View file

Large diffs are not rendered by default.

702 changes: 361 additions & 341 deletions master/Data.List.Relation.Binary.Permutation.Propositional.Properties.html
View file

Large diffs are not rendered by default.

6 changes: 3 additions & 3 deletions master/Data.List.Relation.Binary.Subset.Propositional.Properties.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -83,13 +83,13 @@
<a id="2933" class="Comment">-- See issue #1354 for why these proofs can&#39;t be taken from `Subset`</a>

<a id="⊆-reflexive-↭"></a><a id="3003" href="Data.List.Relation.Binary.Subset.Propositional.Properties.html#3003" class="Function">⊆-reflexive-↭</a> <a id="3017" class="Symbol">:</a> <a id="3019" href="Data.List.Relation.Binary.Permutation.Propositional.html#1304" class="Datatype Operator">_↭_</a> <a id="3023" class="Symbol">{</a><a id="3024" class="Argument">A</a> <a id="3026" class="Symbol">=</a> <a id="3028" href="Data.List.Relation.Binary.Subset.Propositional.Properties.html#1997" class="Generalizable">A</a><a id="3029" class="Symbol">}</a> <a id="3031" href="Relation.Binary.Core.html#1268" class="Function Operator">⇒</a> <a id="3033" href="Data.List.Relation.Binary.Subset.Setoid.html#825" class="Function Operator">_⊆_</a>
<a id="3037" href="Data.List.Relation.Binary.Subset.Propositional.Properties.html#3003" class="Function">⊆-reflexive-↭</a> <a id="3051" href="Data.List.Relation.Binary.Subset.Propositional.Properties.html#3051" class="Bound">xs↭ys</a> <a id="3057" class="Symbol">=</a> <a id="3059" href="Data.List.Relation.Binary.Permutation.Propositional.Properties.html#3467" class="Function">Permutation.∈-resp-↭</a> <a id="3080" href="Data.List.Relation.Binary.Subset.Propositional.Properties.html#3051" class="Bound">xs↭ys</a>
<a id="3037" href="Data.List.Relation.Binary.Subset.Propositional.Properties.html#3003" class="Function">⊆-reflexive-↭</a> <a id="3051" href="Data.List.Relation.Binary.Subset.Propositional.Properties.html#3051" class="Bound">xs↭ys</a> <a id="3057" class="Symbol">=</a> <a id="3059" href="Data.List.Relation.Binary.Permutation.Propositional.Properties.html#3609" class="Function">Permutation.∈-resp-↭</a> <a id="3080" href="Data.List.Relation.Binary.Subset.Propositional.Properties.html#3051" class="Bound">xs↭ys</a>

<a id="⊆-respʳ-↭"></a><a id="3087" href="Data.List.Relation.Binary.Subset.Propositional.Properties.html#3087" class="Function">⊆-respʳ-↭</a> <a id="3097" class="Symbol">:</a> <a id="3099" href="Data.List.Relation.Binary.Subset.Setoid.html#825" class="Function Operator">_⊆_</a> <a id="3103" class="Symbol">{</a><a id="3104" class="Argument">A</a> <a id="3106" class="Symbol">=</a> <a id="3108" href="Data.List.Relation.Binary.Subset.Propositional.Properties.html#1997" class="Generalizable">A</a><a id="3109" class="Symbol">}</a> <a id="3111" href="Relation.Binary.Definitions.html#5314" class="Function Operator">Respectsʳ</a> <a id="3121" href="Data.List.Relation.Binary.Permutation.Propositional.html#1304" class="Datatype Operator">_↭_</a>
<a id="3125" href="Data.List.Relation.Binary.Subset.Propositional.Properties.html#3087" class="Function">⊆-respʳ-↭</a> <a id="3135" href="Data.List.Relation.Binary.Subset.Propositional.Properties.html#3135" class="Bound">xs↭ys</a> <a id="3141" class="Symbol">=</a> <a id="3143" href="Data.List.Relation.Binary.Permutation.Propositional.Properties.html#3467" class="Function">Permutation.∈-resp-↭</a> <a id="3164" href="Data.List.Relation.Binary.Subset.Propositional.Properties.html#3135" class="Bound">xs↭ys</a> <a id="3170" href="Function.Base.html#1115" class="Function Operator">∘_</a>
<a id="3125" href="Data.List.Relation.Binary.Subset.Propositional.Properties.html#3087" class="Function">⊆-respʳ-↭</a> <a id="3135" href="Data.List.Relation.Binary.Subset.Propositional.Properties.html#3135" class="Bound">xs↭ys</a> <a id="3141" class="Symbol">=</a> <a id="3143" href="Data.List.Relation.Binary.Permutation.Propositional.Properties.html#3609" class="Function">Permutation.∈-resp-↭</a> <a id="3164" href="Data.List.Relation.Binary.Subset.Propositional.Properties.html#3135" class="Bound">xs↭ys</a> <a id="3170" href="Function.Base.html#1115" class="Function Operator">∘_</a>

<a id="⊆-respˡ-↭"></a><a id="3174" href="Data.List.Relation.Binary.Subset.Propositional.Properties.html#3174" class="Function">⊆-respˡ-↭</a> <a id="3184" class="Symbol">:</a> <a id="3186" href="Data.List.Relation.Binary.Subset.Setoid.html#825" class="Function Operator">_⊆_</a> <a id="3190" class="Symbol">{</a><a id="3191" class="Argument">A</a> <a id="3193" class="Symbol">=</a> <a id="3195" href="Data.List.Relation.Binary.Subset.Propositional.Properties.html#1997" class="Generalizable">A</a><a id="3196" class="Symbol">}</a> <a id="3198" href="Relation.Binary.Definitions.html#5479" class="Function Operator">Respectsˡ</a> <a id="3208" href="Data.List.Relation.Binary.Permutation.Propositional.html#1304" class="Datatype Operator">_↭_</a>
<a id="3212" href="Data.List.Relation.Binary.Subset.Propositional.Properties.html#3174" class="Function">⊆-respˡ-↭</a> <a id="3222" href="Data.List.Relation.Binary.Subset.Propositional.Properties.html#3222" class="Bound">xs↭ys</a> <a id="3228" class="Symbol">=</a> <a id="3230" href="Function.Base.html#1115" class="Function Operator">_∘</a> <a id="3233" href="Data.List.Relation.Binary.Permutation.Propositional.Properties.html#3467" class="Function">Permutation.∈-resp-↭</a> <a id="3254" class="Symbol">(</a><a id="3255" href="Data.List.Relation.Binary.Permutation.Propositional.html#1718" class="Function">↭-sym</a> <a id="3261" href="Data.List.Relation.Binary.Subset.Propositional.Properties.html#3222" class="Bound">xs↭ys</a><a id="3266" class="Symbol">)</a>
<a id="3212" href="Data.List.Relation.Binary.Subset.Propositional.Properties.html#3174" class="Function">⊆-respˡ-↭</a> <a id="3222" href="Data.List.Relation.Binary.Subset.Propositional.Properties.html#3222" class="Bound">xs↭ys</a> <a id="3228" class="Symbol">=</a> <a id="3230" href="Function.Base.html#1115" class="Function Operator">_∘</a> <a id="3233" href="Data.List.Relation.Binary.Permutation.Propositional.Properties.html#3609" class="Function">Permutation.∈-resp-↭</a> <a id="3254" class="Symbol">(</a><a id="3255" href="Data.List.Relation.Binary.Permutation.Propositional.html#1718" class="Function">↭-sym</a> <a id="3261" href="Data.List.Relation.Binary.Subset.Propositional.Properties.html#3222" class="Bound">xs↭ys</a><a id="3266" class="Symbol">)</a>

<a id="3269" class="Keyword">module</a> <a id="3276" href="Data.List.Relation.Binary.Subset.Propositional.Properties.html#3276" class="Module">_</a> <a id="3278" class="Symbol">(</a><a id="3279" href="Data.List.Relation.Binary.Subset.Propositional.Properties.html#3279" class="Bound">A</a> <a id="3281" class="Symbol">:</a> <a id="3283" href="Agda.Primitive.html#388" class="Primitive">Set</a> <a id="3287" href="Data.List.Relation.Binary.Subset.Propositional.Properties.html#1977" class="Generalizable">a</a><a id="3288" class="Symbol">)</a> <a id="3290" class="Keyword">where</a>

Expand Down
4 changes: 2 additions & 2 deletions master/Data.List.Relation.Ternary.Interleaving.Propositional.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@

<a id="364" class="Keyword">open</a> <a id="369" class="Keyword">import</a> <a id="376" href="Data.List.Base.html" class="Module">Data.List.Base</a> <a id="391" class="Symbol">as</a> <a id="394" class="Module">List</a> <a id="399" class="Keyword">using</a> <a id="405" class="Symbol">(</a><a id="406" href="Agda.Builtin.List.html#147" class="Datatype">List</a><a id="410" class="Symbol">;</a> <a id="412" href="Data.List.Base.html#7808" class="InductiveConstructor">[]</a><a id="414" class="Symbol">;</a> <a id="416" href="Agda.Builtin.List.html#199" class="InductiveConstructor Operator">_∷_</a><a id="419" class="Symbol">;</a> <a id="421" href="Data.List.Base.html#1957" class="Function Operator">_++_</a><a id="425" class="Symbol">)</a>
<a id="427" class="Keyword">open</a> <a id="432" class="Keyword">import</a> <a id="439" href="Data.List.Relation.Binary.Permutation.Propositional.html" class="Module">Data.List.Relation.Binary.Permutation.Propositional</a> <a id="491" class="Symbol">as</a> <a id="494" class="Module">Perm</a> <a id="499" class="Keyword">using</a> <a id="505" class="Symbol">(</a><a id="506" href="Data.List.Relation.Binary.Permutation.Propositional.html#1304" class="Datatype Operator">_↭_</a><a id="509" class="Symbol">)</a>
<a id="511" class="Keyword">open</a> <a id="516" class="Keyword">import</a> <a id="523" href="Data.List.Relation.Binary.Permutation.Propositional.Properties.html" class="Module">Data.List.Relation.Binary.Permutation.Propositional.Properties</a> <a id="586" class="Keyword">using</a> <a id="592" class="Symbol">(</a><a id="593" href="Data.List.Relation.Binary.Permutation.Propositional.Properties.html#6751" class="Function">shift</a><a id="598" class="Symbol">)</a>
<a id="511" class="Keyword">open</a> <a id="516" class="Keyword">import</a> <a id="523" href="Data.List.Relation.Binary.Permutation.Propositional.Properties.html" class="Module">Data.List.Relation.Binary.Permutation.Propositional.Properties</a> <a id="586" class="Keyword">using</a> <a id="592" class="Symbol">(</a><a id="593" href="Data.List.Relation.Binary.Permutation.Propositional.Properties.html#6893" class="Function">shift</a><a id="598" class="Symbol">)</a>
<a id="600" class="Keyword">import</a> <a id="607" href="Data.List.Relation.Ternary.Interleaving.Setoid.html" class="Module">Data.List.Relation.Ternary.Interleaving.Setoid</a> <a id="654" class="Symbol">as</a> <a id="657" class="Module">General</a>
<a id="665" class="Keyword">open</a> <a id="670" class="Keyword">import</a> <a id="677" href="Relation.Binary.PropositionalEquality.Core.html" class="Module">Relation.Binary.PropositionalEquality.Core</a> <a id="720" class="Keyword">using</a> <a id="726" class="Symbol">(</a><a id="727" href="Agda.Builtin.Equality.html#207" class="InductiveConstructor">refl</a><a id="731" class="Symbol">)</a>
<a id="733" class="Keyword">open</a> <a id="738" class="Keyword">import</a> <a id="745" href="Relation.Binary.PropositionalEquality.Properties.html" class="Module">Relation.Binary.PropositionalEquality.Properties</a> <a id="794" class="Keyword">using</a> <a id="800" class="Symbol">(</a><a id="801" href="Relation.Binary.PropositionalEquality.Properties.html#5700" class="Function">setoid</a><a id="807" class="Symbol">)</a>
Expand Down Expand Up @@ -39,6 +39,6 @@
<a id="1431" href="Data.List.Relation.Ternary.Interleaving.Propositional.html#1331" class="Function">toPermutation</a> <a id="1445" class="Symbol">(</a><a id="1446" href="Data.List.Relation.Ternary.Interleaving.Propositional.html#1185" class="InductiveConstructor">consˡ</a> <a id="1452" href="Data.List.Relation.Ternary.Interleaving.Propositional.html#1452" class="Bound">sp</a><a id="1454" class="Symbol">)</a> <a id="1456" class="Symbol">=</a> <a id="1458" href="Data.List.Relation.Binary.Permutation.Propositional.html#1367" class="InductiveConstructor">Perm.prep</a> <a id="1468" class="Symbol">_</a> <a id="1470" class="Symbol">(</a><a id="1471" href="Data.List.Relation.Ternary.Interleaving.Propositional.html#1331" class="Function">toPermutation</a> <a id="1485" href="Data.List.Relation.Ternary.Interleaving.Propositional.html#1452" class="Bound">sp</a><a id="1487" class="Symbol">)</a>
<a id="1489" href="Data.List.Relation.Ternary.Interleaving.Propositional.html#1331" class="Function">toPermutation</a> <a id="1503" class="Symbol">{</a><a id="1504" href="Data.List.Relation.Ternary.Interleaving.Propositional.html#1504" class="Bound">l</a><a id="1505" class="Symbol">}</a> <a id="1507" class="Symbol">{</a><a id="1508" href="Data.List.Relation.Ternary.Interleaving.Propositional.html#1508" class="Bound">r</a> <a id="1510" href="Agda.Builtin.List.html#199" class="InductiveConstructor Operator">∷</a> <a id="1512" href="Data.List.Relation.Ternary.Interleaving.Propositional.html#1512" class="Bound">rs</a><a id="1514" class="Symbol">}</a> <a id="1516" class="Symbol">{</a><a id="1517" href="Data.List.Relation.Ternary.Interleaving.Propositional.html#1517" class="Bound">a</a> <a id="1519" href="Agda.Builtin.List.html#199" class="InductiveConstructor Operator">∷</a> <a id="1521" href="Data.List.Relation.Ternary.Interleaving.Propositional.html#1521" class="Bound">as</a><a id="1523" class="Symbol">}</a> <a id="1525" class="Symbol">(</a><a id="1526" href="Data.List.Relation.Ternary.Interleaving.Propositional.html#1215" class="InductiveConstructor">consʳ</a> <a id="1532" href="Data.List.Relation.Ternary.Interleaving.Propositional.html#1532" class="Bound">sp</a><a id="1534" class="Symbol">)</a> <a id="1536" class="Symbol">=</a> <a id="1538" href="Relation.Binary.Reasoning.Syntax.html#1510" class="Function Operator">begin</a>
<a id="1546" href="Data.List.Relation.Ternary.Interleaving.Propositional.html#1517" class="Bound">a</a> <a id="1548" href="Agda.Builtin.List.html#199" class="InductiveConstructor Operator">∷</a> <a id="1550" href="Data.List.Relation.Ternary.Interleaving.Propositional.html#1521" class="Bound">as</a> <a id="1559" href="Relation.Binary.Reasoning.Syntax.html#9857" class="Function">↭⟨</a> <a id="1562" href="Data.List.Relation.Binary.Permutation.Propositional.html#1367" class="InductiveConstructor">Perm.prep</a> <a id="1572" href="Data.List.Relation.Ternary.Interleaving.Propositional.html#1517" class="Bound">a</a> <a id="1574" class="Symbol">(</a><a id="1575" href="Data.List.Relation.Ternary.Interleaving.Propositional.html#1331" class="Function">toPermutation</a> <a id="1589" href="Data.List.Relation.Ternary.Interleaving.Propositional.html#1532" class="Bound">sp</a><a id="1591" class="Symbol">)</a> <a id="1593" href="Relation.Binary.Reasoning.Syntax.html#9857" class="Function">⟩</a>
<a id="1597" href="Data.List.Relation.Ternary.Interleaving.Propositional.html#1517" class="Bound">a</a> <a id="1599" href="Agda.Builtin.List.html#199" class="InductiveConstructor Operator">∷</a> <a id="1601" href="Data.List.Relation.Ternary.Interleaving.Propositional.html#1504" class="Bound">l</a> <a id="1603" href="Data.List.Base.html#1957" class="Function Operator">++</a> <a id="1606" href="Data.List.Relation.Ternary.Interleaving.Propositional.html#1512" class="Bound">rs</a> <a id="1610" href="Relation.Binary.Reasoning.Syntax.html#9857" class="Function">↭⟨</a> <a id="1613" href="Data.List.Relation.Binary.Permutation.Propositional.html#1718" class="Function">Perm.↭-sym</a> <a id="1624" class="Symbol">(</a><a id="1625" href="Data.List.Relation.Binary.Permutation.Propositional.Properties.html#6751" class="Function">shift</a> <a id="1631" href="Data.List.Relation.Ternary.Interleaving.Propositional.html#1517" class="Bound">a</a> <a id="1633" href="Data.List.Relation.Ternary.Interleaving.Propositional.html#1504" class="Bound">l</a> <a id="1635" href="Data.List.Relation.Ternary.Interleaving.Propositional.html#1512" class="Bound">rs</a><a id="1637" class="Symbol">)</a> <a id="1639" href="Relation.Binary.Reasoning.Syntax.html#9857" class="Function">⟩</a>
<a id="1597" href="Data.List.Relation.Ternary.Interleaving.Propositional.html#1517" class="Bound">a</a> <a id="1599" href="Agda.Builtin.List.html#199" class="InductiveConstructor Operator">∷</a> <a id="1601" href="Data.List.Relation.Ternary.Interleaving.Propositional.html#1504" class="Bound">l</a> <a id="1603" href="Data.List.Base.html#1957" class="Function Operator">++</a> <a id="1606" href="Data.List.Relation.Ternary.Interleaving.Propositional.html#1512" class="Bound">rs</a> <a id="1610" href="Relation.Binary.Reasoning.Syntax.html#9857" class="Function">↭⟨</a> <a id="1613" href="Data.List.Relation.Binary.Permutation.Propositional.html#1718" class="Function">Perm.↭-sym</a> <a id="1624" class="Symbol">(</a><a id="1625" href="Data.List.Relation.Binary.Permutation.Propositional.Properties.html#6893" class="Function">shift</a> <a id="1631" href="Data.List.Relation.Ternary.Interleaving.Propositional.html#1517" class="Bound">a</a> <a id="1633" href="Data.List.Relation.Ternary.Interleaving.Propositional.html#1504" class="Bound">l</a> <a id="1635" href="Data.List.Relation.Ternary.Interleaving.Propositional.html#1512" class="Bound">rs</a><a id="1637" class="Symbol">)</a> <a id="1639" href="Relation.Binary.Reasoning.Syntax.html#9857" class="Function">⟩</a>
<a id="1643" href="Data.List.Relation.Ternary.Interleaving.Propositional.html#1504" class="Bound">l</a> <a id="1645" href="Data.List.Base.html#1957" class="Function Operator">++</a> <a id="1648" href="Data.List.Relation.Ternary.Interleaving.Propositional.html#1517" class="Bound">a</a> <a id="1650" href="Agda.Builtin.List.html#199" class="InductiveConstructor Operator">∷</a> <a id="1652" href="Data.List.Relation.Ternary.Interleaving.Propositional.html#1512" class="Bound">rs</a> <a id="1656" href="Relation.Binary.Reasoning.Syntax.html#12283" class="Function Operator">∎</a>
</pre></body></html>
Loading

0 comments on commit 0c269d9

Please sign in to comment.