Skip to content

Commit ab512d3

Browse files
github-merge-queue[bot]github-merge-queue[bot]
committed
Deploying to gh-pages from @ 7a09f23 🚀
1 parent b3a15bb commit ab512d3

File tree

49 files changed

+6173
-6144
lines changed

Some content is hidden

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

49 files changed

+6173
-6144
lines changed

‎master/Data.Fin.Properties.html‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@
2626
<a id="997" class="Keyword">open</a> <a id="1002" class="Keyword">import</a> <a id="1009" href="Data.Product.Base.html" class="Module">Data.Product.Base</a> <a id="1027" class="Symbol">as</a> <a id="1030" class="Module">Product</a>
2727
<a id="1040" class="Keyword">using</a> <a id="1046" class="Symbol">(</a><a id="1047" href="Data.Product.Base.html#852" class="Function">∃</a><a id="1048" class="Symbol">;</a> <a id="1050" href="Data.Product.Base.html#907" class="Function">∃₂</a><a id="1052" class="Symbol">;</a> <a id="1054" href="Data.Product.Base.html#1618" class="Function Operator">_×_</a><a id="1057" class="Symbol">;</a> <a id="1059" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">_,_</a><a id="1062" class="Symbol">;</a> <a id="1064" href="Data.Product.Base.html#2173" class="Function">map</a><a id="1067" class="Symbol">;</a> <a id="1069" href="Data.Product.Base.html#636" class="Field">proj₁</a><a id="1074" class="Symbol">;</a> <a id="1076" href="Data.Product.Base.html#650" class="Field">proj₂</a><a id="1081" class="Symbol">;</a> <a id="1083" href="Data.Product.Base.html#3109" class="Function">uncurry</a><a id="1090" class="Symbol">;</a> <a id="1092" href="Data.Product.Base.html#2000" class="Function Operator">&lt;_,_&gt;</a><a id="1097" class="Symbol">)</a>
2828
<a id="1099" class="Keyword">open</a> <a id="1104" class="Keyword">import</a> <a id="1111" href="Data.Product.Properties.html" class="Module">Data.Product.Properties</a> <a id="1135" class="Keyword">using</a> <a id="1141" class="Symbol">(</a><a id="1142" href="Data.Product.Properties.html#1945" class="Function">,-injective</a><a id="1153" class="Symbol">)</a>
29-
<a id="1155" class="Keyword">open</a> <a id="1160" class="Keyword">import</a> <a id="1167" href="Data.Product.Algebra.html" class="Module">Data.Product.Algebra</a> <a id="1188" class="Keyword">using</a> <a id="1194" class="Symbol">(</a><a id="1195" href="Data.Product.Algebra.html#1658" class="Function">×-cong</a><a id="1201" class="Symbol">)</a>
29+
<a id="1155" class="Keyword">open</a> <a id="1160" class="Keyword">import</a> <a id="1167" href="Data.Product.Algebra.html" class="Module">Data.Product.Algebra</a> <a id="1188" class="Keyword">using</a> <a id="1194" class="Symbol">(</a><a id="1195" href="Data.Product.Algebra.html#2001" class="Function">×-cong</a><a id="1201" class="Symbol">)</a>
3030
<a id="1203" class="Keyword">open</a> <a id="1208" class="Keyword">import</a> <a id="1215" href="Data.Sum.Base.html" class="Module">Data.Sum.Base</a> <a id="1229" class="Symbol">as</a> <a id="1232" class="Module">Sum</a> <a id="1236" class="Keyword">using</a> <a id="1242" class="Symbol">(</a><a id="1243" href="Data.Sum.Base.html#625" class="Datatype Operator">_⊎_</a><a id="1246" class="Symbol">;</a> <a id="1248" href="Data.Sum.Base.html#675" class="InductiveConstructor">inj₁</a><a id="1252" class="Symbol">;</a> <a id="1254" href="Data.Sum.Base.html#700" class="InductiveConstructor">inj₂</a><a id="1258" class="Symbol">;</a> <a id="1260" href="Data.Sum.Base.html#811" class="Function Operator">[_,_]</a><a id="1265" class="Symbol">;</a> <a id="1267" href="Data.Sum.Base.html#980" class="Function Operator">[_,_]′</a><a id="1273" class="Symbol">)</a>
3131
<a id="1275" class="Keyword">open</a> <a id="1280" class="Keyword">import</a> <a id="1287" href="Data.Sum.Properties.html" class="Module">Data.Sum.Properties</a> <a id="1307" class="Keyword">using</a> <a id="1313" class="Symbol">(</a><a id="1314" href="Data.Sum.Properties.html#1812" class="Function">[,]-map</a><a id="1321" class="Symbol">;</a> <a id="1323" href="Data.Sum.Properties.html#1655" class="Function">[,]-∘</a><a id="1328" class="Symbol">)</a>
3232
<a id="1330" class="Keyword">open</a> <a id="1335" class="Keyword">import</a> <a id="1342" href="Function.Base.html" class="Module">Function.Base</a> <a id="1356" class="Keyword">using</a> <a id="1362" class="Symbol">(</a><a id="1363" href="Function.Base.html#1115" class="Function Operator">_∘_</a><a id="1366" class="Symbol">;</a> <a id="1368" href="Function.Base.html#704" class="Function">id</a><a id="1370" class="Symbol">;</a> <a id="1372" href="Function.Base.html#1974" class="Function Operator">_$_</a><a id="1375" class="Symbol">;</a> <a id="1377" href="Function.Base.html#1638" class="Function">flip</a><a id="1381" class="Symbol">)</a>

‎master/Data.Integer.Divisibility.Signed.html‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -65,9 +65,9 @@
6565
<a id="2290" href="Data.Integer.Divisibility.Signed.html#2249" class="Function">sign-eq</a> <a id="2298" class="Symbol">=</a> <a id="2300" href="Relation.Binary.PropositionalEquality.Core.html#2035" class="Function">sym</a> <a id="2304" href="Function.Base.html#1974" class="Function Operator">$</a> <a id="2306" href="Relation.Binary.Reasoning.Syntax.html#1572" class="Function Operator">begin</a>
6666
<a id="2316" href="Data.Integer.Base.html#1837" class="Function">sign</a> <a id="2321" class="Symbol">(</a><a id="2322" href="Data.Integer.Divisibility.Signed.html#2138" class="Function">s[i*k]◃q</a> <a id="2331" href="Data.Integer.Base.html#5391" class="Function Operator">*</a> <a id="2333" class="Bound">k</a><a id="2334" class="Symbol">)</a> <a id="2354" href="Relation.Binary.Reasoning.Syntax.html#11048" class="Function">≡⟨</a> <a id="2357" href="Data.Integer.Properties.html#52964" class="Function">sign-*</a> <a id="2364" href="Data.Integer.Divisibility.Signed.html#2138" class="Function">s[i*k]◃q</a> <a id="2373" class="Bound">k</a> <a id="2375" href="Relation.Binary.Reasoning.Syntax.html#11048" class="Function">⟩</a>
6767
<a id="2381" href="Data.Integer.Base.html#1837" class="Function">sign</a> <a id="2386" href="Data.Integer.Divisibility.Signed.html#2138" class="Function">s[i*k]◃q</a> <a id="2395" href="Data.Sign.Base.html#764" class="Function Operator">Sign.*</a> <a id="2402" href="Data.Integer.Base.html#1837" class="Function">sign</a> <a id="2407" class="Bound">k</a> <a id="2419" href="Relation.Binary.Reasoning.Syntax.html#11048" class="Function">≡⟨</a> <a id="2422" href="Relation.Binary.PropositionalEquality.Core.html#1481" class="Function">cong</a> <a id="2427" class="Symbol">(</a><a id="2428" href="Data.Sign.Base.html#764" class="Function Operator">Sign._*</a> <a id="2436" class="Symbol">_)</a> <a id="2439" class="Symbol">(</a><a id="2440" href="Data.Integer.Properties.html#24439" class="Function">sign-◃</a> <a id="2447" href="Data.Integer.Divisibility.Signed.html#2106" class="Function">s[i*k]</a> <a id="2454" class="Bound">q</a><a id="2455" class="Symbol">)</a> <a id="2457" href="Relation.Binary.Reasoning.Syntax.html#11048" class="Function">⟩</a>
68-
<a id="2463" href="Data.Integer.Divisibility.Signed.html#2106" class="Function">s[i*k]</a> <a id="2470" href="Data.Sign.Base.html#764" class="Function Operator">Sign.*</a> <a id="2477" href="Data.Integer.Base.html#1837" class="Function">sign</a> <a id="2482" class="Bound">k</a> <a id="2501" href="Relation.Binary.Reasoning.Syntax.html#11048" class="Function">≡⟨</a> <a id="2504" href="Data.Sign.Properties.html#2792" class="Function">Sign.*-assoc</a> <a id="2517" class="Symbol">(</a><a id="2518" href="Data.Integer.Base.html#1837" class="Function">sign</a> <a id="2523" class="Bound">i</a><a id="2524" class="Symbol">)</a> <a id="2526" class="Symbol">(</a><a id="2527" href="Data.Integer.Base.html#1837" class="Function">sign</a> <a id="2532" class="Bound">k</a><a id="2533" class="Symbol">)</a> <a id="2535" class="Symbol">(</a><a id="2536" href="Data.Integer.Base.html#1837" class="Function">sign</a> <a id="2541" class="Bound">k</a><a id="2542" class="Symbol">)</a> <a id="2544" href="Relation.Binary.Reasoning.Syntax.html#11048" class="Function">⟩</a>
69-
<a id="2550" href="Data.Integer.Base.html#1837" class="Function">sign</a> <a id="2555" class="Bound">i</a> <a id="2557" href="Data.Sign.Base.html#764" class="Function Operator">Sign.*</a> <a id="2564" class="Symbol">(</a><a id="2565" href="Data.Integer.Base.html#1837" class="Function">sign</a> <a id="2570" class="Bound">k</a> <a id="2572" href="Data.Sign.Base.html#764" class="Function Operator">Sign.*</a> <a id="2579" href="Data.Integer.Base.html#1837" class="Function">sign</a> <a id="2584" class="Bound">k</a><a id="2585" class="Symbol">)</a> <a id="2588" href="Relation.Binary.Reasoning.Syntax.html#11048" class="Function">≡⟨</a> <a id="2591" href="Relation.Binary.PropositionalEquality.Core.html#1481" class="Function">cong</a> <a id="2596" class="Symbol">(</a><a id="2597" href="Data.Integer.Base.html#1837" class="Function">sign</a> <a id="2602" class="Bound">i</a> <a id="2604" href="Data.Sign.Base.html#764" class="Function Operator">Sign.*_</a><a id="2611" class="Symbol">)</a> <a id="2613" class="Symbol">(</a><a id="2614" href="Data.Sign.Properties.html#2438" class="Function">Sign.s*s≡+</a> <a id="2625" class="Symbol">(</a><a id="2626" href="Data.Integer.Base.html#1837" class="Function">sign</a> <a id="2631" class="Bound">k</a><a id="2632" class="Symbol">))</a> <a id="2635" href="Relation.Binary.Reasoning.Syntax.html#11048" class="Function">⟩</a>
70-
<a id="2641" href="Data.Integer.Base.html#1837" class="Function">sign</a> <a id="2646" class="Bound">i</a> <a id="2648" href="Data.Sign.Base.html#764" class="Function Operator">Sign.*</a> <a id="2655" href="Data.Sign.Base.html#553" class="InductiveConstructor">Sign.+</a> <a id="2679" href="Relation.Binary.Reasoning.Syntax.html#11048" class="Function">≡⟨</a> <a id="2682" href="Data.Sign.Properties.html#2548" class="Function">Sign.*-identityʳ</a> <a id="2699" class="Symbol">(</a><a id="2700" href="Data.Integer.Base.html#1837" class="Function">sign</a> <a id="2705" class="Bound">i</a><a id="2706" class="Symbol">)</a> <a id="2708" href="Relation.Binary.Reasoning.Syntax.html#11048" class="Function">⟩</a>
68+
<a id="2463" href="Data.Integer.Divisibility.Signed.html#2106" class="Function">s[i*k]</a> <a id="2470" href="Data.Sign.Base.html#764" class="Function Operator">Sign.*</a> <a id="2477" href="Data.Integer.Base.html#1837" class="Function">sign</a> <a id="2482" class="Bound">k</a> <a id="2501" href="Relation.Binary.Reasoning.Syntax.html#11048" class="Function">≡⟨</a> <a id="2504" href="Data.Sign.Properties.html#2900" class="Function">Sign.*-assoc</a> <a id="2517" class="Symbol">(</a><a id="2518" href="Data.Integer.Base.html#1837" class="Function">sign</a> <a id="2523" class="Bound">i</a><a id="2524" class="Symbol">)</a> <a id="2526" class="Symbol">(</a><a id="2527" href="Data.Integer.Base.html#1837" class="Function">sign</a> <a id="2532" class="Bound">k</a><a id="2533" class="Symbol">)</a> <a id="2535" class="Symbol">(</a><a id="2536" href="Data.Integer.Base.html#1837" class="Function">sign</a> <a id="2541" class="Bound">k</a><a id="2542" class="Symbol">)</a> <a id="2544" href="Relation.Binary.Reasoning.Syntax.html#11048" class="Function">⟩</a>
69+
<a id="2550" href="Data.Integer.Base.html#1837" class="Function">sign</a> <a id="2555" class="Bound">i</a> <a id="2557" href="Data.Sign.Base.html#764" class="Function Operator">Sign.*</a> <a id="2564" class="Symbol">(</a><a id="2565" href="Data.Integer.Base.html#1837" class="Function">sign</a> <a id="2570" class="Bound">k</a> <a id="2572" href="Data.Sign.Base.html#764" class="Function Operator">Sign.*</a> <a id="2579" href="Data.Integer.Base.html#1837" class="Function">sign</a> <a id="2584" class="Bound">k</a><a id="2585" class="Symbol">)</a> <a id="2588" href="Relation.Binary.Reasoning.Syntax.html#11048" class="Function">≡⟨</a> <a id="2591" href="Relation.Binary.PropositionalEquality.Core.html#1481" class="Function">cong</a> <a id="2596" class="Symbol">(</a><a id="2597" href="Data.Integer.Base.html#1837" class="Function">sign</a> <a id="2602" class="Bound">i</a> <a id="2604" href="Data.Sign.Base.html#764" class="Function Operator">Sign.*_</a><a id="2611" class="Symbol">)</a> <a id="2613" class="Symbol">(</a><a id="2614" href="Data.Sign.Properties.html#2546" class="Function">Sign.s*s≡+</a> <a id="2625" class="Symbol">(</a><a id="2626" href="Data.Integer.Base.html#1837" class="Function">sign</a> <a id="2631" class="Bound">k</a><a id="2632" class="Symbol">))</a> <a id="2635" href="Relation.Binary.Reasoning.Syntax.html#11048" class="Function">⟩</a>
70+
<a id="2641" href="Data.Integer.Base.html#1837" class="Function">sign</a> <a id="2646" class="Bound">i</a> <a id="2648" href="Data.Sign.Base.html#764" class="Function Operator">Sign.*</a> <a id="2655" href="Data.Sign.Base.html#553" class="InductiveConstructor">Sign.+</a> <a id="2679" href="Relation.Binary.Reasoning.Syntax.html#11048" class="Function">≡⟨</a> <a id="2682" href="Data.Sign.Properties.html#2656" class="Function">Sign.*-identityʳ</a> <a id="2699" class="Symbol">(</a><a id="2700" href="Data.Integer.Base.html#1837" class="Function">sign</a> <a id="2705" class="Bound">i</a><a id="2706" class="Symbol">)</a> <a id="2708" href="Relation.Binary.Reasoning.Syntax.html#11048" class="Function">⟩</a>
7171
<a id="2714" href="Data.Integer.Base.html#1837" class="Function">sign</a> <a id="2719" class="Bound">i</a> <a id="2752" href="Relation.Binary.Reasoning.Syntax.html#12345" class="Function Operator">∎</a>
7272
<a id="2758" class="Keyword">where</a> <a id="2764" class="Keyword">open</a> <a id="2769" href="Relation.Binary.PropositionalEquality.Properties.html#6850" class="Module">≡-Reasoning</a>
7373

0 commit comments

Comments
 (0)