Skip to content

Commit 6597947

Browse files
felixwellenfelixwellen
committed
Deploying to gh-pages from @ 294e796 🚀
1 parent bf315db commit 6597947

File tree

1,120 files changed

+167084
-167787
lines changed

Some content is hidden

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

1,120 files changed

+167084
-167787
lines changed

‎Agda.Builtin.Cubical.Sub.html‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@
1212

1313
<a id="255" class="Symbol">{-#</a> <a id="259" class="Keyword">BUILTIN</a> <a id="267" class="Keyword">SUBIN</a> <a id="273" href="Agda.Builtin.Cubical.Sub.html#196" class="Postulate">inS</a> <a id="277" class="Symbol">#-}</a>
1414

15-
<a id="284" class="Comment">-- Sub A φ u is treated as A.</a>
15+
<a id="284" class="Comment">-- Sub A φ u is treated as A.</a>
1616
<a id="316" class="Symbol">{-#</a> <a id="320" class="Keyword">COMPILE</a> <a id="328" class="Keyword">JS</a> <a id="331" href="Agda.Builtin.Cubical.Sub.html#196" class="Postulate">inS</a> <a id="335" class="Pragma">=</a> <a id="337" class="Pragma">_</a> <a id="339" class="Pragma">=&gt;</a> <a id="342" class="Pragma">_</a> <a id="344" class="Pragma">=&gt;</a> <a id="347" class="Pragma">_</a> <a id="349" class="Pragma">=&gt;</a> <a id="352" class="Pragma">x</a> <a id="354" class="Pragma">=&gt;</a> <a id="357" class="Pragma">x</a> <a id="359" class="Symbol">#-}</a>
1717

1818
<a id="366" class="Keyword">primitive</a>

‎Agda.Builtin.Reflection.html‎

Lines changed: 132 additions & 127 deletions
Large diffs are not rendered by default.

‎Agda.Builtin.String.html‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -34,5 +34,5 @@
3434
<a id="1231" class="Symbol">{-#</a> <a id="1235" class="Keyword">COMPILE</a> <a id="1243" class="Keyword">JS</a> <a id="1246" href="Agda.Builtin.String.html#585" class="Primitive">primStringEquality</a> <a id="1265" class="Pragma">=</a> <a id="1267" class="Pragma">function(x)</a> <a id="1279" class="Pragma">{</a> <a id="1281" class="Pragma">return</a> <a id="1288" class="Pragma">function(y)</a> <a id="1300" class="Pragma">{</a> <a id="1302" class="Pragma">return</a> <a id="1309" class="Pragma">x===y;</a> <a id="1316" class="Pragma">};</a> <a id="1319" class="Pragma">}</a> <a id="1321" class="Symbol">#-}</a>
3535
<a id="1325" class="Symbol">{-#</a> <a id="1329" class="Keyword">COMPILE</a> <a id="1337" class="Keyword">JS</a> <a id="1340" href="Agda.Builtin.String.html#631" class="Primitive">primShowChar</a> <a id="1353" class="Pragma">=</a> <a id="1355" class="Pragma">function(x)</a> <a id="1367" class="Pragma">{</a> <a id="1369" class="Pragma">return</a> <a id="1376" class="Pragma">JSON.stringify(x);</a> <a id="1395" class="Pragma">}</a> <a id="1397" class="Symbol">#-}</a>
3636
<a id="1401" class="Symbol">{-#</a> <a id="1405" class="Keyword">COMPILE</a> <a id="1413" class="Keyword">JS</a> <a id="1416" href="Agda.Builtin.String.html#668" class="Primitive">primShowString</a> <a id="1431" class="Pragma">=</a> <a id="1433" class="Pragma">function(x)</a> <a id="1445" class="Pragma">{</a> <a id="1447" class="Pragma">return</a> <a id="1454" class="Pragma">JSON.stringify(x);</a> <a id="1473" class="Pragma">}</a> <a id="1475" class="Symbol">#-}</a>
37-
<a id="1479" class="Symbol">{-#</a> <a id="1483" class="Keyword">COMPILE</a> <a id="1491" class="Keyword">JS</a> <a id="1494" href="Agda.Builtin.String.html#707" class="Primitive">primShowNat</a> <a id="1506" class="Pragma">=</a> <a id="1508" class="Pragma">function(x)</a> <a id="1520" class="Pragma">{</a> <a id="1522" class="Pragma">return</a> <a id="1529" class="Pragma">JSON.stringify(x);</a> <a id="1548" class="Pragma">}</a> <a id="1550" class="Symbol">#-}</a>
37+
<a id="1479" class="Symbol">{-#</a> <a id="1483" class="Keyword">COMPILE</a> <a id="1491" class="Keyword">JS</a> <a id="1494" href="Agda.Builtin.String.html#707" class="Primitive">primShowNat</a> <a id="1506" class="Pragma">=</a> <a id="1508" class="Pragma">function(x)</a> <a id="1520" class="Pragma">{</a> <a id="1522" class="Pragma">return</a> <a id="1529" class="Pragma">x.toString();</a> <a id="1543" class="Pragma">}</a> <a id="1545" class="Symbol">#-}</a>
3838
</pre></body></html>

‎Cubical.Algebra.AbGroup.Base.html‎

Lines changed: 346 additions & 347 deletions
Large diffs are not rendered by default.

‎Cubical.Algebra.AbGroup.Instances.DiffInt.html‎

Lines changed: 18 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -2,26 +2,25 @@
22
<html><head><meta charset="utf-8"><title>Cubical.Algebra.AbGroup.Instances.DiffInt</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Comment">-- It is recommended to use Cubical.Algebra.CommRing.Instances.Int</a>
33
<a id="68" class="Comment">-- instead of this file.</a>
44

5-
<a id="94" class="Symbol">{-#</a> <a id="98" class="Keyword">OPTIONS</a> <a id="106" class="Pragma">--safe</a> <a id="113" class="Symbol">#-}</a>
6-
<a id="117" class="Keyword">module</a> <a id="124" href="Cubical.Algebra.AbGroup.Instances.DiffInt.html" class="Module">Cubical.Algebra.AbGroup.Instances.DiffInt</a> <a id="166" class="Keyword">where</a>
5+
<a id="94" class="Keyword">module</a> <a id="101" href="Cubical.Algebra.AbGroup.Instances.DiffInt.html" class="Module">Cubical.Algebra.AbGroup.Instances.DiffInt</a> <a id="143" class="Keyword">where</a>
76

8-
<a id="173" class="Keyword">open</a> <a id="178" class="Keyword">import</a> <a id="185" href="Cubical.Foundations.Prelude.html" class="Module">Cubical.Foundations.Prelude</a>
9-
<a id="213" class="Keyword">open</a> <a id="218" class="Keyword">import</a> <a id="225" href="Cubical.HITs.SetQuotients.html" class="Module">Cubical.HITs.SetQuotients</a>
7+
<a id="150" class="Keyword">open</a> <a id="155" class="Keyword">import</a> <a id="162" href="Cubical.Foundations.Prelude.html" class="Module">Cubical.Foundations.Prelude</a>
8+
<a id="190" class="Keyword">open</a> <a id="195" class="Keyword">import</a> <a id="202" href="Cubical.HITs.SetQuotients.html" class="Module">Cubical.HITs.SetQuotients</a>
109

11-
<a id="252" class="Keyword">open</a> <a id="257" class="Keyword">import</a> <a id="264" href="Cubical.Algebra.AbGroup.Base.html" class="Module">Cubical.Algebra.AbGroup.Base</a>
12-
<a id="293" class="Keyword">open</a> <a id="298" class="Keyword">import</a> <a id="305" href="Cubical.Data.Int.MoreInts.DiffInt.html" class="Module">Cubical.Data.Int.MoreInts.DiffInt</a>
13-
<a id="341" class="Keyword">renaming</a> <a id="350" class="Symbol">(</a>
14-
<a id="356" href="Cubical.Data.Int.MoreInts.DiffInt.Properties.html#4830" class="Function Operator">_+_</a> <a id="360" class="Symbol">to</a> <a id="363" class="Function Operator">_+ℤ_</a>
15-
<a id="370" class="Symbol">)</a>
10+
<a id="229" class="Keyword">open</a> <a id="234" class="Keyword">import</a> <a id="241" href="Cubical.Algebra.AbGroup.Base.html" class="Module">Cubical.Algebra.AbGroup.Base</a>
11+
<a id="270" class="Keyword">open</a> <a id="275" class="Keyword">import</a> <a id="282" href="Cubical.Data.Int.MoreInts.DiffInt.html" class="Module">Cubical.Data.Int.MoreInts.DiffInt</a>
12+
<a id="318" class="Keyword">renaming</a> <a id="327" class="Symbol">(</a>
13+
<a id="333" href="Cubical.Data.Int.MoreInts.DiffInt.Properties.html#4807" class="Function Operator">_+_</a> <a id="337" class="Symbol">to</a> <a id="340" class="Function Operator">_+ℤ_</a>
14+
<a id="347" class="Symbol">)</a>
1615

17-
<a id="DiffℤasAbGroup"></a><a id="373" href="Cubical.Algebra.AbGroup.Instances.DiffInt.html#373" class="Function">DiffℤasAbGroup</a> <a id="388" class="Symbol">:</a> <a id="390" href="Cubical.Algebra.AbGroup.Base.html#1781" class="Function">AbGroup</a> <a id="398" href="Agda.Primitive.html#915" class="Primitive">ℓ-zero</a>
18-
<a id="405" href="Cubical.Algebra.AbGroup.Instances.DiffInt.html#373" class="Function">DiffℤasAbGroup</a> <a id="420" class="Symbol">=</a> <a id="422" href="Cubical.Algebra.AbGroup.Base.html#2711" class="Function">makeAbGroup</a> <a id="434" class="Symbol">{</a><a id="435" class="Argument">G</a> <a id="437" class="Symbol">=</a> <a id="439" href="Cubical.Data.Int.MoreInts.DiffInt.Base.html#467" class="Function">ℤ</a><a id="440" class="Symbol">}</a>
19-
<a id="471" href="Cubical.HITs.SetQuotients.Base.html#289" class="InductiveConstructor Operator">[</a> <a id="473" class="Symbol">(</a><a id="474" class="Number">0</a> <a id="476" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="478" class="Number">0</a><a id="479" class="Symbol">)</a> <a id="481" href="Cubical.HITs.SetQuotients.Base.html#289" class="InductiveConstructor Operator">]</a>
20-
<a id="512" href="Cubical.Algebra.AbGroup.Instances.DiffInt.html#363" class="Function Operator">_+ℤ_</a>
21-
<a id="546" href="Cubical.Data.Int.MoreInts.DiffInt.Properties.html#6464" class="Function Operator">-ℤ_</a>
22-
<a id="579" href="Cubical.Data.Int.MoreInts.DiffInt.Properties.html#4777" class="Function">ℤ-isSet</a>
23-
<a id="616" href="Cubical.Data.Int.MoreInts.DiffInt.Properties.html#8616" class="Function">+ℤ-assoc</a>
24-
<a id="654" class="Symbol">(λ</a> <a id="657" href="Cubical.Algebra.AbGroup.Instances.DiffInt.html#657" class="Bound">x</a> <a id="659" class="Symbol">→</a> <a id="661" href="Cubical.Data.Int.MoreInts.DiffInt.Properties.html#6147" class="Function">zero-identityʳ</a> <a id="676" class="Number">0</a> <a id="678" href="Cubical.Algebra.AbGroup.Instances.DiffInt.html#657" class="Bound">x</a><a id="679" class="Symbol">)</a>
25-
<a id="710" class="Symbol">(λ</a> <a id="713" href="Cubical.Algebra.AbGroup.Instances.DiffInt.html#713" class="Bound">x</a> <a id="715" class="Symbol">→</a> <a id="717" href="Cubical.Data.Int.MoreInts.DiffInt.Properties.html#8088" class="Function">-ℤ-invʳ</a> <a id="725" href="Cubical.Algebra.AbGroup.Instances.DiffInt.html#713" class="Bound">x</a><a id="726" class="Symbol">)</a>
26-
<a id="757" href="Cubical.Data.Int.MoreInts.DiffInt.Properties.html#8793" class="Function">+ℤ-comm</a>
16+
<a id="DiffℤasAbGroup"></a><a id="350" href="Cubical.Algebra.AbGroup.Instances.DiffInt.html#350" class="Function">DiffℤasAbGroup</a> <a id="365" class="Symbol">:</a> <a id="367" href="Cubical.Algebra.AbGroup.Base.html#1758" class="Function">AbGroup</a> <a id="375" href="Agda.Primitive.html#915" class="Primitive">ℓ-zero</a>
17+
<a id="382" href="Cubical.Algebra.AbGroup.Instances.DiffInt.html#350" class="Function">DiffℤasAbGroup</a> <a id="397" class="Symbol">=</a> <a id="399" href="Cubical.Algebra.AbGroup.Base.html#2688" class="Function">makeAbGroup</a> <a id="411" class="Symbol">{</a><a id="412" class="Argument">G</a> <a id="414" class="Symbol">=</a> <a id="416" href="Cubical.Data.Int.MoreInts.DiffInt.Base.html#444" class="Function">ℤ</a><a id="417" class="Symbol">}</a>
18+
<a id="448" href="Cubical.HITs.SetQuotients.Base.html#266" class="InductiveConstructor Operator">[</a> <a id="450" class="Symbol">(</a><a id="451" class="Number">0</a> <a id="453" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="455" class="Number">0</a><a id="456" class="Symbol">)</a> <a id="458" href="Cubical.HITs.SetQuotients.Base.html#266" class="InductiveConstructor Operator">]</a>
19+
<a id="489" href="Cubical.Algebra.AbGroup.Instances.DiffInt.html#340" class="Function Operator">_+ℤ_</a>
20+
<a id="523" href="Cubical.Data.Int.MoreInts.DiffInt.Properties.html#6441" class="Function Operator">-ℤ_</a>
21+
<a id="556" href="Cubical.Data.Int.MoreInts.DiffInt.Properties.html#4754" class="Function">ℤ-isSet</a>
22+
<a id="593" href="Cubical.Data.Int.MoreInts.DiffInt.Properties.html#8593" class="Function">+ℤ-assoc</a>
23+
<a id="631" class="Symbol">(λ</a> <a id="634" href="Cubical.Algebra.AbGroup.Instances.DiffInt.html#634" class="Bound">x</a> <a id="636" class="Symbol">→</a> <a id="638" href="Cubical.Data.Int.MoreInts.DiffInt.Properties.html#6124" class="Function">zero-identityʳ</a> <a id="653" class="Number">0</a> <a id="655" href="Cubical.Algebra.AbGroup.Instances.DiffInt.html#634" class="Bound">x</a><a id="656" class="Symbol">)</a>
24+
<a id="687" class="Symbol">(λ</a> <a id="690" href="Cubical.Algebra.AbGroup.Instances.DiffInt.html#690" class="Bound">x</a> <a id="692" class="Symbol">→</a> <a id="694" href="Cubical.Data.Int.MoreInts.DiffInt.Properties.html#8065" class="Function">-ℤ-invʳ</a> <a id="702" href="Cubical.Algebra.AbGroup.Instances.DiffInt.html#690" class="Bound">x</a><a id="703" class="Symbol">)</a>
25+
<a id="734" href="Cubical.Data.Int.MoreInts.DiffInt.Properties.html#8770" class="Function">+ℤ-comm</a>
2726
</pre></body></html>

0 commit comments

Comments
 (0)