Skip to content

Commit 40d9240

Browse files
github-merge-queue[bot]github-merge-queue[bot]
committed
Deploying to gh-pages from @ 7848967 🚀
1 parent cd70bc2 commit 40d9240

File tree

73 files changed

+2765
-2741
lines changed

Some content is hidden

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

73 files changed

+2765
-2741
lines changed

‎master/Codata.Musical.Colist.Infinite-merge.html‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@
1717
<a id="612" class="Keyword">open</a> <a id="617" class="Keyword">import</a> <a id="624" href="Data.Product.Base.html" class="Module">Data.Product.Base</a> <a id="642" class="Symbol">as</a> <a id="645" class="Module">Product</a> <a id="653" class="Keyword">using</a> <a id="659" class="Symbol">(</a><a id="660" href="Data.Product.Base.html#1618" class="Function Operator">_×_</a><a id="663" class="Symbol">;</a> <a id="665" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">_,_</a><a id="668" class="Symbol">;</a> <a id="670" href="Data.Product.Base.html#852" class="Function">∃</a><a id="671" class="Symbol">;</a> <a id="673" href="Data.Product.Base.html#907" class="Function">∃₂</a><a id="675" class="Symbol">;</a> <a id="677" href="Data.Product.Base.html#636" class="Field">proj₁</a><a id="682" class="Symbol">;</a> <a id="684" href="Data.Product.Base.html#650" class="Field">proj₂</a><a id="689" class="Symbol">)</a>
1818
<a id="691" class="Keyword">open</a> <a id="696" class="Keyword">import</a> <a id="703" href="Data.Sum.Base.html" class="Module">Data.Sum.Base</a> <a id="717" class="Keyword">using</a> <a id="723" class="Symbol">(</a><a id="724" href="Data.Sum.Base.html#625" class="Datatype Operator">_⊎_</a><a id="727" class="Symbol">;</a> <a id="729" href="Data.Sum.Base.html#675" class="InductiveConstructor">inj₁</a><a id="733" class="Symbol">;</a> <a id="735" href="Data.Sum.Base.html#700" class="InductiveConstructor">inj₂</a><a id="739" class="Symbol">;</a> <a id="741" href="Data.Sum.Base.html#980" class="Function Operator">[_,_]′</a><a id="747" class="Symbol">)</a>
1919
<a id="749" class="Keyword">open</a> <a id="754" class="Keyword">import</a> <a id="761" href="Data.Sum.Properties.html" class="Module">Data.Sum.Properties</a> <a id="781" class="Keyword">using</a> <a id="787" class="Symbol">(</a><a id="788" href="Data.Sum.Properties.html#871" class="Function">inj₁-injective</a><a id="802" class="Symbol">;</a> <a id="804" href="Data.Sum.Properties.html#960" class="Function">inj₂-injective</a><a id="818" class="Symbol">)</a>
20-
<a id="820" class="Keyword">open</a> <a id="825" class="Keyword">import</a> <a id="832" href="Data.Sum.Function.Propositional.html" class="Module">Data.Sum.Function.Propositional</a> <a id="864" class="Keyword">using</a> <a id="870" class="Symbol">(</a><a id="871" href="Data.Sum.Function.Propositional.html#3067" class="Function Operator">_⊎-cong_</a><a id="879" class="Symbol">)</a>
20+
<a id="820" class="Keyword">open</a> <a id="825" class="Keyword">import</a> <a id="832" href="Data.Sum.Function.Propositional.html" class="Module">Data.Sum.Function.Propositional</a> <a id="864" class="Keyword">using</a> <a id="870" class="Symbol">(</a><a id="871" href="Data.Sum.Function.Propositional.html#3307" class="Function Operator">_⊎-cong_</a><a id="879" class="Symbol">)</a>
2121
<a id="881" class="Keyword">open</a> <a id="886" class="Keyword">import</a> <a id="893" href="Function.Base.html" class="Module">Function.Base</a> <a id="907" class="Keyword">using</a> <a id="913" class="Symbol">(</a><a id="914" href="Function.Base.html#1115" class="Function Operator">_∘_</a><a id="917" class="Symbol">;</a> <a id="919" href="Function.Base.html#4486" class="Function Operator">_∋_</a><a id="922" class="Symbol">;</a> <a id="924" href="Function.Base.html#704" class="Function">id</a><a id="926" class="Symbol">;</a> <a id="928" href="Function.Base.html#3626" class="Function Operator">_∘′_</a><a id="932" class="Symbol">;</a> <a id="934" href="Function.Base.html#1974" class="Function Operator">_$_</a><a id="937" class="Symbol">;</a> <a id="939" href="Function.Base.html#6209" class="Function Operator">_on_</a><a id="943" class="Symbol">)</a>
2222
<a id="945" class="Keyword">open</a> <a id="950" class="Keyword">import</a> <a id="957" href="Function.Bundles.html" class="Module">Function.Bundles</a> <a id="974" class="Keyword">using</a> <a id="980" class="Symbol">(</a><a id="981" href="Function.Bundles.html#7340" class="Record">Inverse</a><a id="988" class="Symbol">;</a> <a id="990" href="Function.Bundles.html#2415" class="Record">Injection</a><a id="999" class="Symbol">;</a> <a id="1001" href="Function.Bundles.html#12701" class="Function Operator">_↔_</a><a id="1004" class="Symbol">;</a> <a id="1006" href="Function.Bundles.html#14924" class="Function">mk↔ₛ′</a><a id="1011" class="Symbol">)</a>
2323
<a id="1013" class="Keyword">open</a> <a id="1018" class="Keyword">import</a> <a id="1025" href="Function.Properties.Inverse.html" class="Module">Function.Properties.Inverse</a> <a id="1053" class="Keyword">using</a> <a id="1059" class="Symbol">(</a><a id="1060" href="Function.Properties.Inverse.html#1698" class="Function">↔-refl</a><a id="1066" class="Symbol">;</a> <a id="1068" href="Function.Properties.Inverse.html#1739" class="Function">↔-sym</a><a id="1073" class="Symbol">;</a> <a id="1075" href="Function.Properties.Inverse.html#3309" class="Function">↔⇒↣</a><a id="1078" class="Symbol">)</a>
@@ -97,7 +97,7 @@
9797
<a id="3069" href="Codata.Musical.Colist.Infinite-merge.html#2979" class="Function">Any-⋎P</a> <a id="3076" class="Symbol">{</a><a id="3077" class="Argument">P</a> <a id="3079" class="Symbol">=</a> <a id="3081" href="Codata.Musical.Colist.Infinite-merge.html#3081" class="Bound">P</a><a id="3082" class="Symbol">}</a> <a id="3084" href="Codata.Musical.Colist.Infinite-merge.html#3084" class="Bound">xs</a> <a id="3087" class="Symbol">{</a><a id="3088" href="Codata.Musical.Colist.Infinite-merge.html#3088" class="Bound">ys</a><a id="3090" class="Symbol">}</a> <a id="3092" class="Symbol">=</a>
9898
<a id="3098" href="Codata.Musical.Colist.Relation.Unary.Any.html#766" class="Datatype">Any</a> <a id="3102" href="Codata.Musical.Colist.Infinite-merge.html#3081" class="Bound">P</a> <a id="3104" href="Codata.Musical.Colist.Infinite-merge.html#2388" class="Function Operator">⟦</a> <a id="3106" href="Codata.Musical.Colist.Infinite-merge.html#2033" class="Function">program</a> <a id="3114" href="Codata.Musical.Colist.Infinite-merge.html#3084" class="Bound">xs</a> <a id="3117" href="Codata.Musical.Colist.Infinite-merge.html#1892" class="InductiveConstructor Operator">⋎</a> <a id="3119" href="Codata.Musical.Colist.Infinite-merge.html#3088" class="Bound">ys</a> <a id="3122" href="Codata.Musical.Colist.Infinite-merge.html#2388" class="Function Operator">⟧P</a> <a id="3140" href="Relation.Binary.Reasoning.Syntax.html#9687" class="Function">↔⟨</a> <a id="3143" href="Codata.Musical.Colist.Relation.Unary.Any.Properties.html#1820" class="Function">Any-cong</a> <a id="3152" href="Function.Properties.Inverse.html#1698" class="Function">↔-refl</a> <a id="3159" class="Symbol">(</a><a id="3160" href="Codata.Musical.Colist.Infinite-merge.html#2544" class="Function">⋎-homP</a> <a id="3167" class="Symbol">(</a><a id="3168" href="Codata.Musical.Colist.Infinite-merge.html#2033" class="Function">program</a> <a id="3176" href="Codata.Musical.Colist.Infinite-merge.html#3084" class="Bound">xs</a><a id="3178" class="Symbol">))</a> <a id="3181" href="Relation.Binary.Reasoning.Syntax.html#9687" class="Function">⟩</a>
9999
<a id="3187" href="Codata.Musical.Colist.Relation.Unary.Any.html#766" class="Datatype">Any</a> <a id="3191" href="Codata.Musical.Colist.Infinite-merge.html#3081" class="Bound">P</a> <a id="3193" class="Symbol">(</a><a id="3194" href="Codata.Musical.Colist.Infinite-merge.html#2388" class="Function Operator">⟦</a> <a id="3196" href="Codata.Musical.Colist.Infinite-merge.html#2033" class="Function">program</a> <a id="3204" href="Codata.Musical.Colist.Infinite-merge.html#3084" class="Bound">xs</a> <a id="3207" href="Codata.Musical.Colist.Infinite-merge.html#2388" class="Function Operator">⟧P</a> <a id="3210" href="Codata.Musical.Colist.Base.html#2138" class="Function Operator">Colist.⋎</a> <a id="3219" href="Codata.Musical.Colist.Infinite-merge.html#2388" class="Function Operator">⟦</a> <a id="3221" href="Codata.Musical.Colist.Infinite-merge.html#3088" class="Bound">ys</a> <a id="3224" href="Codata.Musical.Colist.Infinite-merge.html#2388" class="Function Operator">⟧P</a><a id="3226" class="Symbol">)</a> <a id="3229" href="Relation.Binary.Reasoning.Syntax.html#9687" class="Function">↔⟨</a> <a id="3232" href="Codata.Musical.Colist.Relation.Unary.Any.Properties.html#4176" class="Function">Any-⋎</a> <a id="3238" class="Symbol">_</a> <a id="3240" href="Relation.Binary.Reasoning.Syntax.html#9687" class="Function">⟩</a>
100-
<a id="3246" class="Symbol">(</a><a id="3247" href="Codata.Musical.Colist.Relation.Unary.Any.html#766" class="Datatype">Any</a> <a id="3251" href="Codata.Musical.Colist.Infinite-merge.html#3081" class="Bound">P</a> <a id="3253" href="Codata.Musical.Colist.Infinite-merge.html#2388" class="Function Operator">⟦</a> <a id="3255" href="Codata.Musical.Colist.Infinite-merge.html#2033" class="Function">program</a> <a id="3263" href="Codata.Musical.Colist.Infinite-merge.html#3084" class="Bound">xs</a> <a id="3266" href="Codata.Musical.Colist.Infinite-merge.html#2388" class="Function Operator">⟧P</a> <a id="3269" href="Data.Sum.Base.html#625" class="Datatype Operator">⊎</a> <a id="3271" href="Codata.Musical.Colist.Relation.Unary.Any.html#766" class="Datatype">Any</a> <a id="3275" href="Codata.Musical.Colist.Infinite-merge.html#3081" class="Bound">P</a> <a id="3277" href="Codata.Musical.Colist.Infinite-merge.html#2388" class="Function Operator">⟦</a> <a id="3279" href="Codata.Musical.Colist.Infinite-merge.html#3088" class="Bound">ys</a> <a id="3282" href="Codata.Musical.Colist.Infinite-merge.html#2388" class="Function Operator">⟧P</a><a id="3284" class="Symbol">)</a> <a id="3288" href="Relation.Binary.Reasoning.Syntax.html#9687" class="Function">↔⟨</a> <a id="3291" href="Codata.Musical.Colist.Relation.Unary.Any.Properties.html#1820" class="Function">Any-cong</a> <a id="3300" href="Function.Properties.Inverse.html#1698" class="Function">↔-refl</a> <a id="3307" class="Symbol">(</a><a id="3308" href="Codata.Musical.Colist.Infinite-merge.html#2847" class="Function">⟦program⟧P</a> <a id="3319" class="Symbol">_)</a> <a id="3322" href="Data.Sum.Function.Propositional.html#3067" class="Function Operator">⊎-cong</a> <a id="3329" class="Symbol">(_</a> <a id="3332" href="Relation.Binary.Reasoning.Syntax.html#12345" class="Function Operator">∎</a><a id="3333" class="Symbol">)</a> <a id="3335" href="Relation.Binary.Reasoning.Syntax.html#9687" class="Function">⟩</a>
100+
<a id="3246" class="Symbol">(</a><a id="3247" href="Codata.Musical.Colist.Relation.Unary.Any.html#766" class="Datatype">Any</a> <a id="3251" href="Codata.Musical.Colist.Infinite-merge.html#3081" class="Bound">P</a> <a id="3253" href="Codata.Musical.Colist.Infinite-merge.html#2388" class="Function Operator">⟦</a> <a id="3255" href="Codata.Musical.Colist.Infinite-merge.html#2033" class="Function">program</a> <a id="3263" href="Codata.Musical.Colist.Infinite-merge.html#3084" class="Bound">xs</a> <a id="3266" href="Codata.Musical.Colist.Infinite-merge.html#2388" class="Function Operator">⟧P</a> <a id="3269" href="Data.Sum.Base.html#625" class="Datatype Operator">⊎</a> <a id="3271" href="Codata.Musical.Colist.Relation.Unary.Any.html#766" class="Datatype">Any</a> <a id="3275" href="Codata.Musical.Colist.Infinite-merge.html#3081" class="Bound">P</a> <a id="3277" href="Codata.Musical.Colist.Infinite-merge.html#2388" class="Function Operator">⟦</a> <a id="3279" href="Codata.Musical.Colist.Infinite-merge.html#3088" class="Bound">ys</a> <a id="3282" href="Codata.Musical.Colist.Infinite-merge.html#2388" class="Function Operator">⟧P</a><a id="3284" class="Symbol">)</a> <a id="3288" href="Relation.Binary.Reasoning.Syntax.html#9687" class="Function">↔⟨</a> <a id="3291" href="Codata.Musical.Colist.Relation.Unary.Any.Properties.html#1820" class="Function">Any-cong</a> <a id="3300" href="Function.Properties.Inverse.html#1698" class="Function">↔-refl</a> <a id="3307" class="Symbol">(</a><a id="3308" href="Codata.Musical.Colist.Infinite-merge.html#2847" class="Function">⟦program⟧P</a> <a id="3319" class="Symbol">_)</a> <a id="3322" href="Data.Sum.Function.Propositional.html#3307" class="Function Operator">⊎-cong</a> <a id="3329" class="Symbol">(_</a> <a id="3332" href="Relation.Binary.Reasoning.Syntax.html#12345" class="Function Operator">∎</a><a id="3333" class="Symbol">)</a> <a id="3335" href="Relation.Binary.Reasoning.Syntax.html#9687" class="Function">⟩</a>
101101
<a id="3341" class="Symbol">(</a><a id="3342" href="Codata.Musical.Colist.Relation.Unary.Any.html#766" class="Datatype">Any</a> <a id="3346" href="Codata.Musical.Colist.Infinite-merge.html#3081" class="Bound">P</a> <a id="3348" href="Codata.Musical.Colist.Infinite-merge.html#3084" class="Bound">xs</a> <a id="3351" href="Data.Sum.Base.html#625" class="Datatype Operator">⊎</a> <a id="3353" href="Codata.Musical.Colist.Relation.Unary.Any.html#766" class="Datatype">Any</a> <a id="3357" href="Codata.Musical.Colist.Infinite-merge.html#3081" class="Bound">P</a> <a id="3359" href="Codata.Musical.Colist.Infinite-merge.html#2388" class="Function Operator">⟦</a> <a id="3361" href="Codata.Musical.Colist.Infinite-merge.html#3088" class="Bound">ys</a> <a id="3364" href="Codata.Musical.Colist.Infinite-merge.html#2388" class="Function Operator">⟧P</a><a id="3366" class="Symbol">)</a> <a id="3383" href="Relation.Binary.Reasoning.Syntax.html#12345" class="Function Operator">∎</a>
102102
<a id="3389" class="Keyword">where</a> <a id="3395" class="Keyword">open</a> <a id="3400" href="Function.Related.Propositional.html#9123" class="Module">Related.EquationalReasoning</a>
103103

0 commit comments

Comments
 (0)