Skip to content

Commit

Permalink
Deploying to gh-pages from @ 6a1ae77 🚀
Browse files Browse the repository at this point in the history
  • Loading branch information
@github-merge-queue
github-merge-queue[bot] committed Dec 24, 2024
1 parent 3c4de83 commit 9623092
Show file tree
Hide file tree
Showing 19 changed files with 922 additions and 929 deletions.
8 changes: 4 additions & 4 deletions master/Data.List.Effectful.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,8 +13,8 @@
<a id="335" class="Keyword">open</a> <a id="340" class="Keyword">import</a> <a id="347" href="Data.List.Base.html" class="Module">Data.List.Base</a>
<a id="364" class="Keyword">using</a> <a id="370" class="Symbol">(</a><a id="371" href="Agda.Builtin.List.html#147" class="Datatype">List</a><a id="375" class="Symbol">;</a> <a id="377" href="Data.List.Base.html#1634" class="Function">map</a><a id="380" class="Symbol">;</a> <a id="382" href="Data.List.Base.html#5205" class="Function Operator">[_]</a><a id="385" class="Symbol">;</a> <a id="387" href="Data.List.Base.html#4479" class="Function">ap</a><a id="389" class="Symbol">;</a> <a id="391" href="Data.List.Base.html#7599" class="InductiveConstructor">[]</a><a id="393" class="Symbol">;</a> <a id="395" href="Agda.Builtin.List.html#199" class="InductiveConstructor Operator">_∷_</a><a id="398" class="Symbol">;</a> <a id="400" href="Data.List.Base.html#1734" class="Function Operator">_++_</a><a id="404" class="Symbol">;</a> <a id="406" href="Data.List.Base.html#4350" class="Function">concat</a><a id="412" class="Symbol">;</a> <a id="414" href="Data.List.Base.html#4406" class="Function">concatMap</a><a id="423" class="Symbol">)</a>
<a id="425" class="Keyword">open</a> <a id="430" class="Keyword">import</a> <a id="437" href="Data.List.Properties.html" class="Module">Data.List.Properties</a>
<a id="460" class="Keyword">using</a> <a id="466" class="Symbol">(</a><a id="467" href="Data.List.Properties.html#5457" class="Function">++-identityʳ</a><a id="479" class="Symbol">;</a> <a id="481" href="Data.List.Properties.html#5269" class="Function">++-assoc</a><a id="489" class="Symbol">;</a> <a id="491" href="Data.List.Properties.html#4022" class="Function">map-cong</a><a id="499" class="Symbol">;</a> <a id="501" href="Data.List.Properties.html#26868" class="Function">concatMap-cong</a><a id="515" class="Symbol">;</a> <a id="517" href="Data.List.Properties.html#27314" class="Function">map-concatMap</a><a id="530" class="Symbol">;</a>
<a id="536" href="Data.List.Properties.html#26995" class="Function">concatMap-pure</a><a id="550" class="Symbol">)</a>
<a id="460" class="Keyword">using</a> <a id="466" class="Symbol">(</a><a id="467" href="Data.List.Properties.html#5457" class="Function">++-identityʳ</a><a id="479" class="Symbol">;</a> <a id="481" href="Data.List.Properties.html#5269" class="Function">++-assoc</a><a id="489" class="Symbol">;</a> <a id="491" href="Data.List.Properties.html#4022" class="Function">map-cong</a><a id="499" class="Symbol">;</a> <a id="501" href="Data.List.Properties.html#26868" class="Function">concatMap-cong</a><a id="515" class="Symbol">;</a> <a id="517" href="Data.List.Properties.html#27218" class="Function">map-concatMap</a><a id="530" class="Symbol">;</a>
<a id="536" href="Data.List.Properties.html#26989" class="Function">concatMap-pure</a><a id="550" class="Symbol">)</a>
<a id="552" class="Keyword">open</a> <a id="557" class="Keyword">import</a> <a id="564" href="Effect.Choice.html" class="Module">Effect.Choice</a> <a id="578" class="Keyword">using</a> <a id="584" class="Symbol">(</a><a id="585" href="Effect.Choice.html#414" class="Record">RawChoice</a><a id="594" class="Symbol">)</a>
<a id="596" class="Keyword">open</a> <a id="601" class="Keyword">import</a> <a id="608" href="Effect.Empty.html" class="Module">Effect.Empty</a> <a id="621" class="Keyword">using</a> <a id="627" class="Symbol">(</a><a id="628" href="Effect.Empty.html#384" class="Record">RawEmpty</a><a id="636" class="Symbol">)</a>
<a id="638" class="Keyword">open</a> <a id="643" class="Keyword">import</a> <a id="650" href="Effect.Functor.html" class="Module">Effect.Functor</a> <a id="665" class="Keyword">using</a> <a id="671" class="Symbol">(</a><a id="672" href="Effect.Functor.html#579" class="Record">RawFunctor</a><a id="682" class="Symbol">)</a>
Expand Down Expand Up @@ -217,9 +217,9 @@
<a id="6505" class="Symbol">(</a><a id="6506" href="Data.List.Effectful.html#6457" class="Bound">fs</a> <a id="6509" href="Effect.Applicative.html#1605" class="Function Operator">⊛</a> <a id="6511" href="Data.List.Effectful.html#6477" class="Bound">as</a><a id="6513" class="Symbol">)</a> <a id="6515" href="Agda.Builtin.Equality.html#150" class="Datatype Operator">≡</a> <a id="6517" class="Symbol">(</a><a id="6518" href="Data.List.Effectful.html#6457" class="Bound">fs</a> <a id="6521" href="Effect.Monad.html#933" class="Function Operator">&gt;&gt;=</a> <a id="6525" href="Data.List.Effectful.html#5576" class="Function">pam</a> <a id="6529" href="Data.List.Effectful.html#6477" class="Bound">as</a><a id="6531" class="Symbol">)</a>
<a id="6535" href="Data.List.Effectful.html#6423" class="Function">unfold-⊛</a> <a id="6544" href="Data.List.Effectful.html#6544" class="Bound">fs</a> <a id="6547" href="Data.List.Effectful.html#6547" class="Bound">as</a> <a id="6550" class="Symbol">=</a> <a id="6552" href="Relation.Binary.Reasoning.Syntax.html#1572" class="Function Operator">begin</a>
<a id="6562" href="Data.List.Effectful.html#6544" class="Bound">fs</a> <a id="6565" href="Effect.Applicative.html#1605" class="Function Operator">⊛</a> <a id="6567" href="Data.List.Effectful.html#6547" class="Bound">as</a>
<a id="6576" href="Relation.Binary.Reasoning.Syntax.html#11140" class="Function">≡⟨</a> <a id="6579" href="Data.List.Properties.html#26868" class="Function">concatMap-cong</a> <a id="6594" class="Symbol">(λ</a> <a id="6597" href="Data.List.Effectful.html#6597" class="Bound">f</a> <a id="6599" class="Symbol">→</a> <a id="6601" href="Relation.Binary.PropositionalEquality.Core.html#1339" class="Function">≡.cong</a> <a id="6608" class="Symbol">(</a><a id="6609" href="Data.List.Base.html#1634" class="Function">map</a> <a id="6613" href="Data.List.Effectful.html#6597" class="Bound">f</a><a id="6614" class="Symbol">)</a> <a id="6616" class="Symbol">(</a><a id="6617" href="Data.List.Properties.html#26995" class="Function">concatMap-pure</a> <a id="6632" href="Data.List.Effectful.html#6547" class="Bound">as</a><a id="6634" class="Symbol">))</a> <a id="6637" href="Data.List.Effectful.html#6544" class="Bound">fs</a> <a id="6640" href="Relation.Binary.Reasoning.Syntax.html#11140" class="Function">⟨</a>
<a id="6576" href="Relation.Binary.Reasoning.Syntax.html#11140" class="Function">≡⟨</a> <a id="6579" href="Data.List.Properties.html#26868" class="Function">concatMap-cong</a> <a id="6594" class="Symbol">(λ</a> <a id="6597" href="Data.List.Effectful.html#6597" class="Bound">f</a> <a id="6599" class="Symbol">→</a> <a id="6601" href="Relation.Binary.PropositionalEquality.Core.html#1339" class="Function">≡.cong</a> <a id="6608" class="Symbol">(</a><a id="6609" href="Data.List.Base.html#1634" class="Function">map</a> <a id="6613" href="Data.List.Effectful.html#6597" class="Bound">f</a><a id="6614" class="Symbol">)</a> <a id="6616" class="Symbol">(</a><a id="6617" href="Data.List.Properties.html#26989" class="Function">concatMap-pure</a> <a id="6632" href="Data.List.Effectful.html#6547" class="Bound">as</a><a id="6634" class="Symbol">))</a> <a id="6637" href="Data.List.Effectful.html#6544" class="Bound">fs</a> <a id="6640" href="Relation.Binary.Reasoning.Syntax.html#11140" class="Function">⟨</a>
<a id="6646" href="Data.List.Base.html#4406" class="Function">concatMap</a> <a id="6656" class="Symbol">(λ</a> <a id="6659" href="Data.List.Effectful.html#6659" class="Bound">f</a> <a id="6661" class="Symbol">→</a> <a id="6663" href="Data.List.Base.html#1634" class="Function">map</a> <a id="6667" href="Data.List.Effectful.html#6659" class="Bound">f</a> <a id="6669" class="Symbol">(</a><a id="6670" href="Data.List.Base.html#4406" class="Function">concatMap</a> <a id="6680" href="Effect.Applicative.html#1147" class="Function">pure</a> <a id="6685" href="Data.List.Effectful.html#6547" class="Bound">as</a><a id="6687" class="Symbol">))</a> <a id="6690" href="Data.List.Effectful.html#6544" class="Bound">fs</a>
<a id="6699" href="Relation.Binary.Reasoning.Syntax.html#11048" class="Function">≡⟨</a> <a id="6702" href="Data.List.Properties.html#26868" class="Function">concatMap-cong</a> <a id="6717" class="Symbol">(λ</a> <a id="6720" href="Data.List.Effectful.html#6720" class="Bound">f</a> <a id="6722" class="Symbol">→</a> <a id="6724" href="Data.List.Properties.html#27314" class="Function">map-concatMap</a> <a id="6738" href="Data.List.Effectful.html#6720" class="Bound">f</a> <a id="6740" href="Effect.Applicative.html#1147" class="Function">pure</a> <a id="6745" href="Data.List.Effectful.html#6547" class="Bound">as</a><a id="6747" class="Symbol">)</a> <a id="6749" href="Data.List.Effectful.html#6544" class="Bound">fs</a> <a id="6752" href="Relation.Binary.Reasoning.Syntax.html#11048" class="Function">⟩</a>
<a id="6699" href="Relation.Binary.Reasoning.Syntax.html#11048" class="Function">≡⟨</a> <a id="6702" href="Data.List.Properties.html#26868" class="Function">concatMap-cong</a> <a id="6717" class="Symbol">(λ</a> <a id="6720" href="Data.List.Effectful.html#6720" class="Bound">f</a> <a id="6722" class="Symbol">→</a> <a id="6724" href="Data.List.Properties.html#27218" class="Function">map-concatMap</a> <a id="6738" href="Data.List.Effectful.html#6720" class="Bound">f</a> <a id="6740" href="Effect.Applicative.html#1147" class="Function">pure</a> <a id="6745" href="Data.List.Effectful.html#6547" class="Bound">as</a><a id="6747" class="Symbol">)</a> <a id="6749" href="Data.List.Effectful.html#6544" class="Bound">fs</a> <a id="6752" href="Relation.Binary.Reasoning.Syntax.html#11048" class="Function">⟩</a>
<a id="6758" href="Data.List.Base.html#4406" class="Function">concatMap</a> <a id="6768" class="Symbol">(λ</a> <a id="6771" href="Data.List.Effectful.html#6771" class="Bound">f</a> <a id="6773" class="Symbol">→</a> <a id="6775" href="Data.List.Base.html#4406" class="Function">concatMap</a> <a id="6785" class="Symbol">(λ</a> <a id="6788" href="Data.List.Effectful.html#6788" class="Bound">x</a> <a id="6790" class="Symbol">→</a> <a id="6792" href="Effect.Applicative.html#1147" class="Function">pure</a> <a id="6797" class="Symbol">(</a><a id="6798" href="Data.List.Effectful.html#6771" class="Bound">f</a> <a id="6800" href="Data.List.Effectful.html#6788" class="Bound">x</a><a id="6801" class="Symbol">))</a> <a id="6804" href="Data.List.Effectful.html#6547" class="Bound">as</a><a id="6806" class="Symbol">)</a> <a id="6808" href="Data.List.Effectful.html#6544" class="Bound">fs</a>
<a id="6817" href="Relation.Binary.Reasoning.Syntax.html#11079" class="Function">≡⟨⟩</a>
<a id="6825" class="Symbol">(</a><a id="6826" href="Data.List.Effectful.html#6544" class="Bound">fs</a> <a id="6829" href="Effect.Monad.html#933" class="Function Operator">&gt;&gt;=</a> <a id="6833" href="Data.List.Effectful.html#5576" class="Function">pam</a> <a id="6837" href="Data.List.Effectful.html#6547" class="Bound">as</a><a id="6839" class="Symbol">)</a>
Expand Down
Loading

0 comments on commit 9623092

Please sign in to comment.