Commit [Automated by Make]

rahulc29 · Oct 5, 2023 · ee2674e · ee2674e
1 parent 6d7cce9
commit ee2674e
Show file tree

Hide file tree

Showing 48 changed files with 5,778 additions and 343 deletions.
diff --git a/#foo.agda# b/#foo.agda#
@@ -0,0 +1,2 @@
+A → A ⇀ A
+♯ A → ♯ A → ♯ A
diff --git a/Makefile b/Makefile
@@ -0,0 +1,10 @@
+check:
+	cd src
+	agda --html --html-dir=docs ./index.agda
+
+commit_message = Commit [Automated by Make]
+commit:
+	git add . && git commit -m '${commit_message}'
+
+push : commit
+	git push origin master
diff --git a/Makefile~ b/Makefile~
@@ -0,0 +1,10 @@
+check:
+	cd src
+	agda --html --html-dir=docs ./index.agda
+
+commit_message = Commit [Automated by Make]
+commit: check
+	git add . && git commit -m '${commit_message}'
+
+push : commit
+	git push origin master
diff --git a/docs/Cubical.Data.Fin.Base.html b/docs/Cubical.Data.Fin.Base.html
diff --git a/docs/Cubical.Data.Fin.Literals.html b/docs/Cubical.Data.Fin.Literals.html
@@ -0,0 +1,20 @@
+<!DOCTYPE HTML>
+<html><head><meta charset="utf-8"><title>Cubical.Data.Fin.Literals</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--no-exact-split</a> <a id="30" class="Pragma">--safe</a> <a id="37" class="Symbol">#-}</a>
+<a id="41" class="Keyword">module</a> <a id="48" href="Cubical.Data.Fin.Literals.html" class="Module">Cubical.Data.Fin.Literals</a> <a id="74" class="Keyword">where</a>
+
+<a id="81" class="Keyword">open</a> <a id="86" class="Keyword">import</a> <a id="93" href="Agda.Builtin.Nat.html" class="Module">Agda.Builtin.Nat</a>
+  <a id="112" class="Keyword">using</a> <a id="118" class="Symbol">(</a><a id="119" href="Agda.Builtin.Nat.html#217" class="InductiveConstructor">suc</a><a id="122" class="Symbol">)</a>
+<a id="124" class="Keyword">open</a> <a id="129" class="Keyword">import</a> <a id="136" href="Agda.Builtin.FromNat.html" class="Module">Agda.Builtin.FromNat</a>
+  <a id="159" class="Keyword">renaming</a> <a id="168" class="Symbol">(</a><a id="169" href="Agda.Builtin.FromNat.html#179" class="Record">Number</a> <a id="176" class="Symbol">to</a> <a id="179" class="Record">HasFromNat</a><a id="189" class="Symbol">)</a>
+<a id="191" class="Keyword">open</a> <a id="196" class="Keyword">import</a> <a id="203" href="Cubical.Data.Fin.Base.html" class="Module">Cubical.Data.Fin.Base</a>
+  <a id="227" class="Keyword">using</a> <a id="233" class="Symbol">(</a><a id="234" href="Cubical.Data.Fin.Base.html#826" class="Function">Fin</a><a id="237" class="Symbol">;</a> <a id="239" href="Cubical.Data.Fin.Base.html#1554" class="Function">fromℕ≤</a><a id="245" class="Symbol">)</a>
+<a id="247" class="Keyword">open</a> <a id="252" class="Keyword">import</a> <a id="259" href="Cubical.Data.Nat.Order.Recursive.html" class="Module">Cubical.Data.Nat.Order.Recursive</a>
+  <a id="294" class="Keyword">using</a> <a id="300" class="Symbol">(</a><a id="301" href="Cubical.Data.Nat.Order.Recursive.html#546" class="Function Operator">_≤_</a><a id="304" class="Symbol">)</a>
+
+<a id="307" class="Keyword">instance</a>
+  <a id="fromNatFin"></a><a id="318" href="Cubical.Data.Fin.Literals.html#318" class="Function">fromNatFin</a> <a id="329" class="Symbol">:</a> <a id="331" class="Symbol">{</a><a id="332" href="Cubical.Data.Fin.Literals.html#332" class="Bound">n</a> <a id="334" class="Symbol">:</a> <a id="336" class="Symbol">_}</a> <a id="339" class="Symbol">→</a> <a id="341" href="Cubical.Data.Fin.Literals.html#179" class="Record">HasFromNat</a> <a id="352" class="Symbol">(</a><a id="353" href="Cubical.Data.Fin.Base.html#826" class="Function">Fin</a> <a id="357" class="Symbol">(</a><a id="358" href="Agda.Builtin.Nat.html#217" class="InductiveConstructor">suc</a> <a id="362" href="Cubical.Data.Fin.Literals.html#332" class="Bound">n</a><a id="363" class="Symbol">))</a>
+  <a id="368" href="Cubical.Data.Fin.Literals.html#318" class="Function">fromNatFin</a> <a id="379" class="Symbol">{</a><a id="380" href="Cubical.Data.Fin.Literals.html#380" class="Bound">n</a><a id="381" class="Symbol">}</a> <a id="383" class="Symbol">=</a> <a id="385" class="Keyword">record</a>
+    <a id="396" class="Symbol">{</a> <a id="398" href="Agda.Builtin.FromNat.html#235" class="Field">Constraint</a> <a id="409" class="Symbol">=</a> <a id="411" class="Symbol">λ</a> <a id="413" href="Cubical.Data.Fin.Literals.html#413" class="Bound">m</a> <a id="415" class="Symbol">→</a> <a id="417" href="Cubical.Data.Fin.Literals.html#413" class="Bound">m</a> <a id="419" href="Cubical.Data.Nat.Order.Recursive.html#546" class="Function Operator">≤</a> <a id="421" href="Cubical.Data.Fin.Literals.html#380" class="Bound">n</a>
+    <a id="427" class="Symbol">;</a> <a id="429" href="Agda.Builtin.FromNat.html#264" class="Field">fromNat</a>    <a id="440" class="Symbol">=</a> <a id="442" class="Symbol">λ</a> <a id="444" href="Cubical.Data.Fin.Literals.html#444" class="Bound">m</a> <a id="446" class="Symbol">⦃</a> <a id="448" href="Cubical.Data.Fin.Literals.html#448" class="Bound">m≤n</a> <a id="452" class="Symbol">⦄</a> <a id="454" class="Symbol">→</a> <a id="456" href="Cubical.Data.Fin.Base.html#1554" class="Function">fromℕ≤</a> <a id="463" href="Cubical.Data.Fin.Literals.html#444" class="Bound">m</a> <a id="465" href="Cubical.Data.Fin.Literals.html#380" class="Bound">n</a> <a id="467" href="Cubical.Data.Fin.Literals.html#448" class="Bound">m≤n</a>
+    <a id="475" class="Symbol">}</a>
+</pre></body></html>