Deploying to gh-pages from @ a6da449 🚀

master/Codata.Sized.Colist.Properties.html

@@ -24,7 +24,7 @@
 <a id="910" class="Keyword">open</a> <a id="915" class="Keyword">import</a> <a id="922" href="Data.List.Base.html" class="Module">Data.List.Base</a> <a id="937" class="Symbol">as</a> <a id="940" class="Module">List</a> <a id="945" class="Keyword">using</a> <a id="951" class="Symbol">(</a><a id="952" href="Agda.Builtin.List.html#147" class="Datatype">List</a><a id="956" class="Symbol">;</a> <a id="958" href="Data.List.Base.html#7599" class="InductiveConstructor">[]</a><a id="960" class="Symbol">;</a> <a id="962" href="Agda.Builtin.List.html#199" class="InductiveConstructor Operator">_∷_</a><a id="965" class="Symbol">)</a>
 <a id="967" class="Keyword">open</a> <a id="972" class="Keyword">import</a> <a id="979" href="Data.List.NonEmpty.html" class="Module">Data.List.NonEmpty</a> <a id="998" class="Symbol">as</a> <a id="1001" class="Module">List⁺</a> <a id="1007" class="Keyword">using</a> <a id="1013" class="Symbol">(</a><a id="1014" href="Data.List.NonEmpty.Base.html#1229" class="Record">List⁺</a><a id="1019" class="Symbol">;</a> <a id="1021" href="Data.List.NonEmpty.Base.html#1275" class="InductiveConstructor Operator">_∷_</a><a id="1024" class="Symbol">)</a>
 <a id="1026" class="Keyword">import</a> <a id="1033" href="Data.List.Scans.Base.html" class="Module">Data.List.Scans.Base</a> <a id="1054" class="Symbol">as</a> <a id="1057" class="Module">Scans</a>
-<a id="1063" class="Keyword">open</a> <a id="1068" class="Keyword">import</a> <a id="1075" href="Data.List.Relation.Binary.Equality.Propositional.html" class="Module">Data.List.Relation.Binary.Equality.Propositional</a> <a id="1124" class="Keyword">using</a> <a id="1130" class="Symbol">(</a><a id="1131" href="Data.List.Relation.Binary.Equality.Setoid.html#1749" class="Function">≋-refl</a><a id="1137" class="Symbol">)</a>
+<a id="1063" class="Keyword">open</a> <a id="1068" class="Keyword">import</a> <a id="1075" href="Data.List.Relation.Binary.Equality.Propositional.html" class="Module">Data.List.Relation.Binary.Equality.Propositional</a> <a id="1124" class="Keyword">using</a> <a id="1130" class="Symbol">(</a><a id="1131" href="Data.List.Relation.Binary.Equality.Setoid.html#1810" class="Function">≋-refl</a><a id="1137" class="Symbol">)</a>
 <a id="1139" class="Keyword">open</a> <a id="1144" class="Keyword">import</a> <a id="1151" href="Data.Maybe.Base.html" class="Module">Data.Maybe.Base</a> <a id="1167" class="Symbol">as</a> <a id="1170" class="Module">Maybe</a> <a id="1176" class="Keyword">using</a> <a id="1182" class="Symbol">(</a><a id="1183" href="Agda.Builtin.Maybe.html#135" class="Datatype">Maybe</a><a id="1188" class="Symbol">;</a> <a id="1190" href="Agda.Builtin.Maybe.html#194" class="InductiveConstructor">nothing</a><a id="1197" class="Symbol">;</a> <a id="1199" href="Agda.Builtin.Maybe.html#173" class="InductiveConstructor">just</a><a id="1203" class="Symbol">)</a>
 <a id="1205" class="Keyword">import</a> <a id="1212" href="Data.Maybe.Properties.html" class="Module">Data.Maybe.Properties</a> <a id="1234" class="Symbol">as</a> <a id="1237" class="Module">Maybe</a>
 <a id="1243" class="Keyword">open</a> <a id="1248" class="Keyword">import</a> <a id="1255" href="Data.Maybe.Relation.Unary.All.html" class="Module">Data.Maybe.Relation.Unary.All</a> <a id="1285" class="Keyword">using</a> <a id="1291" class="Symbol">(</a><a id="1292" href="Data.Maybe.Relation.Unary.All.html#950" class="Datatype">All</a><a id="1295" class="Symbol">;</a> <a id="1297" href="Data.Maybe.Relation.Unary.All.html#1061" class="InductiveConstructor">nothing</a><a id="1304" class="Symbol">;</a> <a id="1306" href="Data.Maybe.Relation.Unary.All.html#1020" class="InductiveConstructor">just</a><a id="1310" class="Symbol">)</a>
@@ -318,7 +318,7 @@
                     <a id="12864" href="Codata.Sized.Colist.Properties.html#1760" class="Generalizable">i</a> <a id="12866" href="Codata.Sized.Colist.Bisimilarity.html#2759" class="Function Operator">⊢</a> <a id="12868" href="Codata.Sized.Colist.html#3470" class="Function">concat</a> <a id="12875" class="Symbol">(</a><a id="12876" href="Codata.Sized.Colist.html#3599" class="Function">fromStream</a> <a id="12887" href="Codata.Sized.Colist.Properties.html#12816" class="Bound">ass</a><a id="12890" class="Symbol">)</a> <a id="12892" href="Codata.Sized.Colist.Bisimilarity.html#2759" class="Function Operator">≈</a> <a id="12894" href="Codata.Sized.Colist.html#3599" class="Function">fromStream</a> <a id="12905" class="Symbol">(</a><a id="12906" href="Codata.Sized.Stream.html#2786" class="Function">Stream.concat</a> <a id="12920" href="Codata.Sized.Colist.Properties.html#12816" class="Bound">ass</a><a id="12923" class="Symbol">)</a>
 <a id="12925" href="Codata.Sized.Colist.Properties.html#12795" class="Function">fromStream-concat</a> <a id="12943" class="Symbol">(</a><a id="12944" href="Codata.Sized.Colist.Properties.html#12944" class="Bound">as</a><a id="12946" class="Symbol">@(</a><a id="12948" href="Codata.Sized.Colist.Properties.html#12948" class="Bound">a</a> <a id="12950" href="Data.List.NonEmpty.Base.html#1275" class="InductiveConstructor Operator">∷</a> <a id="12952" class="Symbol">_)</a> <a id="12955" href="Codata.Sized.Stream.html#1021" class="InductiveConstructor Operator">∷</a> <a id="12957" href="Codata.Sized.Colist.Properties.html#12957" class="Bound">ass</a><a id="12960" class="Symbol">)</a> <a id="12962" class="Symbol">=</a> <a id="12964" href="Relation.Binary.Reasoning.Syntax.html#1572" class="Function Operator">begin</a>
   <a id="12972" href="Codata.Sized.Colist.html#3470" class="Function">concat</a> <a id="12979" class="Symbol">(</a><a id="12980" href="Codata.Sized.Colist.html#3599" class="Function">fromStream</a> <a id="12991" class="Symbol">(</a><a id="12992" href="Codata.Sized.Colist.Properties.html#12944" class="Bound">as</a> <a id="12995" href="Codata.Sized.Stream.html#1021" class="InductiveConstructor Operator">∷</a> <a id="12997" href="Codata.Sized.Colist.Properties.html#12957" class="Bound">ass</a><a id="13000" class="Symbol">))</a>
-    <a id="13007" href="Relation.Binary.Reasoning.Syntax.html#7111" class="Function">≈⟨</a> <a id="13010" href="Agda.Builtin.Equality.html#207" class="InductiveConstructor">≡.refl</a> <a id="13017" href="Codata.Sized.Colist.Bisimilarity.html#1252" class="InductiveConstructor Operator">∷</a> <a id="13019" class="Symbol">(λ</a> <a id="13022" class="Symbol">{</a> <a id="13024" class="Symbol">.</a><a id="13025" href="Codata.Sized.Thunk.html#556" class="Field">force</a> <a id="13031" class="Symbol">→</a> <a id="13033" href="Codata.Sized.Colist.Bisimilarity.html#2194" class="Function">++⁺</a> <a id="13037" href="Data.List.Relation.Binary.Equality.Setoid.html#1749" class="Function">≋-refl</a> <a id="13044" class="Symbol">(</a><a id="13045" href="Codata.Sized.Colist.Properties.html#12795" class="Function">fromStream-concat</a> <a id="13063" class="Symbol">(</a><a id="13064" href="Codata.Sized.Colist.Properties.html#12957" class="Bound">ass</a> <a id="13068" class="Symbol">.</a><a id="13069" href="Codata.Sized.Thunk.html#556" class="Field">force</a><a id="13074" class="Symbol">))})</a> <a id="13079" href="Relation.Binary.Reasoning.Syntax.html#7111" class="Function">⟩</a>
+    <a id="13007" href="Relation.Binary.Reasoning.Syntax.html#7111" class="Function">≈⟨</a> <a id="13010" href="Agda.Builtin.Equality.html#207" class="InductiveConstructor">≡.refl</a> <a id="13017" href="Codata.Sized.Colist.Bisimilarity.html#1252" class="InductiveConstructor Operator">∷</a> <a id="13019" class="Symbol">(λ</a> <a id="13022" class="Symbol">{</a> <a id="13024" class="Symbol">.</a><a id="13025" href="Codata.Sized.Thunk.html#556" class="Field">force</a> <a id="13031" class="Symbol">→</a> <a id="13033" href="Codata.Sized.Colist.Bisimilarity.html#2194" class="Function">++⁺</a> <a id="13037" href="Data.List.Relation.Binary.Equality.Setoid.html#1810" class="Function">≋-refl</a> <a id="13044" class="Symbol">(</a><a id="13045" href="Codata.Sized.Colist.Properties.html#12795" class="Function">fromStream-concat</a> <a id="13063" class="Symbol">(</a><a id="13064" href="Codata.Sized.Colist.Properties.html#12957" class="Bound">ass</a> <a id="13068" class="Symbol">.</a><a id="13069" href="Codata.Sized.Thunk.html#556" class="Field">force</a><a id="13074" class="Symbol">))})</a> <a id="13079" href="Relation.Binary.Reasoning.Syntax.html#7111" class="Function">⟩</a>
   <a id="13083" href="Codata.Sized.Colist.Properties.html#12948" class="Bound">a</a> <a id="13085" href="Codata.Sized.Colist.html#1401" class="InductiveConstructor Operator">∷</a> <a id="13087" class="Symbol">_</a>
     <a id="13093" href="Relation.Binary.Reasoning.Syntax.html#7111" class="Function">≈⟨</a> <a id="13096" href="Codata.Sized.Colist.Bisimilarity.html#2952" class="Function">sym</a> <a id="13100" class="Symbol">(</a><a id="13101" href="Codata.Sized.Colist.Properties.html#12558" class="Function">fromStream-⁺++</a> <a id="13116" href="Codata.Sized.Colist.Properties.html#12944" class="Bound">as</a> <a id="13119" class="Symbol">_)</a> <a id="13122" href="Relation.Binary.Reasoning.Syntax.html#7111" class="Function">⟩</a>
   <a id="13126" href="Codata.Sized.Colist.html#3599" class="Function">fromStream</a> <a id="13137" class="Symbol">(</a><a id="13138" href="Codata.Sized.Stream.html#2786" class="Function">Stream.concat</a> <a id="13152" class="Symbol">(</a><a id="13153" href="Codata.Sized.Colist.Properties.html#12944" class="Bound">as</a> <a id="13156" href="Codata.Sized.Stream.html#1021" class="InductiveConstructor Operator">∷</a> <a id="13158" href="Codata.Sized.Colist.Properties.html#12957" class="Bound">ass</a><a id="13161" class="Symbol">))</a> <a id="13164" href="Relation.Binary.Reasoning.Syntax.html#12345" class="Function Operator">∎</a> <a id="13166" class="Keyword">where</a> <a id="13172" class="Keyword">open</a> <a id="13177" href="Codata.Sized.Colist.Bisimilarity.html#3470" class="Module">≈-Reasoning</a>