Skip to content

Commit

Permalink
Deploying to gh-pages from @ b429588 🚀
Browse files Browse the repository at this point in the history
  • Loading branch information
@github-merge-queue
github-merge-queue[bot] committed Dec 29, 2024
1 parent ecc34b4 commit 7167a49
Show file tree
Hide file tree
Showing 12 changed files with 976 additions and 954 deletions.
4 changes: 2 additions & 2 deletions master/Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -169,12 +169,12 @@

<a id="6324" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6324" class="Function">inits⁺</a> <a id="6331" class="Symbol">:</a> <a id="6333" class="Symbol">∀</a> <a id="6335" class="Symbol">{</a><a id="6336" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6336" class="Bound">as</a><a id="6338" class="Symbol">}</a> <a id="6340" class="Symbol">→</a> <a id="6342" href="Data.List.Relation.Binary.Pointwise.Base.html#884" class="Datatype">Pointwise</a> <a id="6352" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6302" class="Bound">R</a> <a id="6354" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6336" class="Bound">as</a> <a id="6357" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6336" class="Bound">as</a> <a id="6360" class="Symbol">→</a> <a id="6362" href="Data.List.Relation.Unary.All.html#1644" class="Datatype">All</a> <a id="6366" class="Symbol">(</a><a id="6367" href="Function.Base.html#1638" class="Function">flip</a> <a id="6372" class="Symbol">(</a><a id="6373" href="Data.List.Relation.Binary.Prefix.Heterogeneous.html#704" class="Datatype">Prefix</a> <a id="6380" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6302" class="Bound">R</a><a id="6381" class="Symbol">)</a> <a id="6383" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6336" class="Bound">as</a><a id="6385" class="Symbol">)</a> <a id="6387" class="Symbol">(</a><a id="6388" href="Data.List.Base.html#5517" class="Function">inits</a> <a id="6394" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6336" class="Bound">as</a><a id="6396" class="Symbol">)</a>
<a id="6400" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6324" class="Function">inits⁺</a> <a id="6407" href="Data.List.Relation.Binary.Pointwise.Base.html#993" class="InductiveConstructor">[]</a> <a id="6416" class="Symbol">=</a> <a id="6418" href="Data.List.Relation.Binary.Prefix.Heterogeneous.html#757" class="InductiveConstructor">[]</a> <a id="6421" href="Data.List.Relation.Unary.All.html#1724" class="InductiveConstructor Operator">∷</a> <a id="6423" href="Data.List.Relation.Unary.All.html#1707" class="InductiveConstructor">[]</a>
<a id="6428" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6324" class="Function">inits⁺</a> <a id="6435" class="Symbol">(</a><a id="6436" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6436" class="Bound">r</a> <a id="6438" href="Data.List.Relation.Binary.Pointwise.Base.html#1019" class="InductiveConstructor Operator">∷</a> <a id="6440" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6440" class="Bound">rs</a><a id="6442" class="Symbol">)</a> <a id="6444" class="Symbol">=</a> <a id="6446" href="Data.List.Relation.Binary.Prefix.Heterogeneous.html#757" class="InductiveConstructor">[]</a> <a id="6449" href="Data.List.Relation.Unary.All.html#1724" class="InductiveConstructor Operator">∷</a> <a id="6451" href="Data.List.Relation.Unary.All.Properties.html#12029" class="Function">All.map⁺</a> <a id="6460" class="Symbol">(</a><a id="6461" href="Data.List.Relation.Unary.All.html#3133" class="Function">All.map</a> <a id="6469" class="Symbol">(</a><a id="6470" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6436" class="Bound">r</a> <a id="6472" href="Data.List.Relation.Binary.Prefix.Heterogeneous.html#789" class="InductiveConstructor Operator">∷_</a><a id="6474" class="Symbol">)</a> <a id="6476" class="Symbol">(</a><a id="6477" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6324" class="Function">inits⁺</a> <a id="6484" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6440" class="Bound">rs</a><a id="6486" class="Symbol">))</a>
<a id="6428" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6324" class="Function">inits⁺</a> <a id="6435" class="Symbol">(</a><a id="6436" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6436" class="Bound">r</a> <a id="6438" href="Data.List.Relation.Binary.Pointwise.Base.html#1019" class="InductiveConstructor Operator">∷</a> <a id="6440" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6440" class="Bound">rs</a><a id="6442" class="Symbol">)</a> <a id="6444" class="Symbol">=</a> <a id="6446" href="Data.List.Relation.Binary.Prefix.Heterogeneous.html#757" class="InductiveConstructor">[]</a> <a id="6449" href="Data.List.Relation.Unary.All.html#1724" class="InductiveConstructor Operator">∷</a> <a id="6451" href="Data.List.Relation.Unary.All.Properties.html#11879" class="Function">All.map⁺</a> <a id="6460" class="Symbol">(</a><a id="6461" href="Data.List.Relation.Unary.All.html#3133" class="Function">All.map</a> <a id="6469" class="Symbol">(</a><a id="6470" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6436" class="Bound">r</a> <a id="6472" href="Data.List.Relation.Binary.Prefix.Heterogeneous.html#789" class="InductiveConstructor Operator">∷_</a><a id="6474" class="Symbol">)</a> <a id="6476" class="Symbol">(</a><a id="6477" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6324" class="Function">inits⁺</a> <a id="6484" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6440" class="Bound">rs</a><a id="6486" class="Symbol">))</a>

<a id="6492" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6492" class="Function">inits⁻</a> <a id="6499" class="Symbol">:</a> <a id="6501" class="Symbol">∀</a> <a id="6503" class="Symbol">{</a><a id="6504" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6504" class="Bound">as</a><a id="6506" class="Symbol">}</a> <a id="6508" class="Symbol">→</a> <a id="6510" href="Data.List.Relation.Unary.All.html#1644" class="Datatype">All</a> <a id="6514" class="Symbol">(</a><a id="6515" href="Function.Base.html#1638" class="Function">flip</a> <a id="6520" class="Symbol">(</a><a id="6521" href="Data.List.Relation.Binary.Prefix.Heterogeneous.html#704" class="Datatype">Prefix</a> <a id="6528" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6302" class="Bound">R</a><a id="6529" class="Symbol">)</a> <a id="6531" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6504" class="Bound">as</a><a id="6533" class="Symbol">)</a> <a id="6535" class="Symbol">(</a><a id="6536" href="Data.List.Base.html#5517" class="Function">inits</a> <a id="6542" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6504" class="Bound">as</a><a id="6544" class="Symbol">)</a> <a id="6546" class="Symbol">→</a> <a id="6548" href="Data.List.Relation.Binary.Pointwise.Base.html#884" class="Datatype">Pointwise</a> <a id="6558" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6302" class="Bound">R</a> <a id="6560" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6504" class="Bound">as</a> <a id="6563" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6504" class="Bound">as</a>
<a id="6568" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6492" class="Function">inits⁻</a> <a id="6575" class="Symbol">{</a><a id="6576" class="Argument">as</a> <a id="6579" class="Symbol">=</a> <a id="6581" href="Agda.Builtin.List.html#184" class="InductiveConstructor">[]</a><a id="6583" class="Symbol">}</a> <a id="6589" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6589" class="Bound">rs</a> <a id="6598" class="Symbol">=</a> <a id="6600" href="Data.List.Relation.Binary.Pointwise.Base.html#993" class="InductiveConstructor">[]</a>
<a id="6605" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6492" class="Function">inits⁻</a> <a id="6612" class="Symbol">{</a><a id="6613" class="Argument">as</a> <a id="6616" class="Symbol">=</a> <a id="6618" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6618" class="Bound">a</a> <a id="6620" href="Agda.Builtin.List.html#199" class="InductiveConstructor Operator">∷</a> <a id="6622" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6622" class="Bound">as</a><a id="6624" class="Symbol">}</a> <a id="6626" class="Symbol">(</a><a id="6627" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6627" class="Bound">r</a> <a id="6629" href="Data.List.Relation.Unary.All.html#1724" class="InductiveConstructor Operator">∷</a> <a id="6631" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6631" class="Bound">rs</a><a id="6633" class="Symbol">)</a> <a id="6635" class="Symbol">=</a>
<a id="6641" class="Keyword">let</a> <a id="6645" class="Symbol">(</a><a id="6646" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6646" class="Bound">hd</a> <a id="6649" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="6651" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6651" class="Bound">tls</a><a id="6654" class="Symbol">)</a> <a id="6656" class="Symbol">=</a> <a id="6658" href="Data.List.Relation.Unary.All.html#3574" class="Function">All.unzip</a> <a id="6668" class="Symbol">(</a><a id="6669" href="Data.List.Relation.Unary.All.html#3133" class="Function">All.map</a> <a id="6677" href="Data.List.Relation.Binary.Prefix.Heterogeneous.html#1221" class="Function">uncons</a> <a id="6684" class="Symbol">(</a><a id="6685" href="Data.List.Relation.Unary.All.Properties.html#12134" class="Function">All.map⁻</a> <a id="6694" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6631" class="Bound">rs</a><a id="6696" class="Symbol">))</a> <a id="6699" class="Keyword">in</a>
<a id="6641" class="Keyword">let</a> <a id="6645" class="Symbol">(</a><a id="6646" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6646" class="Bound">hd</a> <a id="6649" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="6651" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6651" class="Bound">tls</a><a id="6654" class="Symbol">)</a> <a id="6656" class="Symbol">=</a> <a id="6658" href="Data.List.Relation.Unary.All.html#3574" class="Function">All.unzip</a> <a id="6668" class="Symbol">(</a><a id="6669" href="Data.List.Relation.Unary.All.html#3133" class="Function">All.map</a> <a id="6677" href="Data.List.Relation.Binary.Prefix.Heterogeneous.html#1221" class="Function">uncons</a> <a id="6684" class="Symbol">(</a><a id="6685" href="Data.List.Relation.Unary.All.Properties.html#11984" class="Function">All.map⁻</a> <a id="6694" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6631" class="Bound">rs</a><a id="6696" class="Symbol">))</a> <a id="6699" class="Keyword">in</a>
<a id="6706" href="Data.List.Relation.Unary.All.html#5949" class="Function">All.lookup</a> <a id="6717" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6646" class="Bound">hd</a> <a id="6720" class="Symbol">(</a><a id="6721" href="Data.List.Membership.Propositional.Properties.html#13421" class="Function">[]∈inits</a> <a id="6730" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6622" class="Bound">as</a><a id="6732" class="Symbol">)</a> <a id="6734" href="Data.List.Relation.Binary.Pointwise.Base.html#1019" class="InductiveConstructor Operator">∷</a> <a id="6736" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6492" class="Function">inits⁻</a> <a id="6743" href="Data.List.Relation.Binary.Prefix.Heterogeneous.Properties.html#6651" class="Bound">tls</a>

<a id="6748" class="Comment">------------------------------------------------------------------------</a>
Expand Down
Loading

0 comments on commit 7167a49

Please sign in to comment.