Skip to content

Commit

Permalink
Deploying to gh-pages from @ 4de6b69 🚀
Browse files Browse the repository at this point in the history
  • Loading branch information
@mortberg
mortberg committed Nov 9, 2023
1 parent e60d022 commit 061ff07
Show file tree
Hide file tree
Showing 2 changed files with 93 additions and 85 deletions.
4 changes: 4 additions & 0 deletions Cubical.Data.Fin.Recursive.Base.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -33,4 +33,8 @@
<a id="627" class="Symbol">→</a> <a id="629" class="Symbol">(</a><a id="630" href="Cubical.Data.Fin.Recursive.Base.html#630" class="Bound">fn</a> <a id="633" class="Symbol">:</a> <a id="635" href="Cubical.Data.Fin.Recursive.Base.html#287" class="Function">Fin</a> <a id="639" href="Cubical.Data.Fin.Recursive.Base.html#381" class="Generalizable">k</a><a id="640" class="Symbol">)</a> <a id="642" class="Symbol">→</a> <a id="644" href="Cubical.Data.Fin.Recursive.Base.html#518" class="Bound">P</a> <a id="646" href="Cubical.Data.Fin.Recursive.Base.html#630" class="Bound">fn</a>
<a id="649" href="Cubical.Data.Fin.Recursive.Base.html#507" class="Function">elim</a> <a id="654" class="Symbol">{</a><a id="655" class="Argument">k</a> <a id="657" class="Symbol">=</a> <a id="659" href="Agda.Builtin.Nat.html#234" class="InductiveConstructor">suc</a> <a id="663" href="Cubical.Data.Fin.Recursive.Base.html#663" class="Bound">k</a><a id="664" class="Symbol">}</a> <a id="666" href="Cubical.Data.Fin.Recursive.Base.html#666" class="Bound">P</a> <a id="668" href="Cubical.Data.Fin.Recursive.Base.html#668" class="Bound">fz</a> <a id="671" href="Cubical.Data.Fin.Recursive.Base.html#671" class="Bound">fs</a> <a id="674" href="Cubical.Data.Fin.Recursive.Base.html#253" class="InductiveConstructor">zero</a> <a id="679" class="Symbol">=</a> <a id="681" href="Cubical.Data.Fin.Recursive.Base.html#668" class="Bound">fz</a>
<a id="684" href="Cubical.Data.Fin.Recursive.Base.html#507" class="Function">elim</a> <a id="689" class="Symbol">{</a><a id="690" class="Argument">k</a> <a id="692" class="Symbol">=</a> <a id="694" href="Agda.Builtin.Nat.html#234" class="InductiveConstructor">suc</a> <a id="698" href="Cubical.Data.Fin.Recursive.Base.html#698" class="Bound">k</a><a id="699" class="Symbol">}</a> <a id="701" href="Cubical.Data.Fin.Recursive.Base.html#701" class="Bound">P</a> <a id="703" href="Cubical.Data.Fin.Recursive.Base.html#703" class="Bound">fz</a> <a id="706" href="Cubical.Data.Fin.Recursive.Base.html#706" class="Bound">fs</a> <a id="709" class="Symbol">(</a><a id="710" href="Cubical.Data.Fin.Recursive.Base.html#269" class="InductiveConstructor">suc</a> <a id="714" href="Cubical.Data.Fin.Recursive.Base.html#714" class="Bound">x</a><a id="715" class="Symbol">)</a> <a id="717" class="Symbol">=</a> <a id="719" href="Cubical.Data.Fin.Recursive.Base.html#706" class="Bound">fs</a> <a id="722" href="Cubical.Data.Fin.Recursive.Base.html#714" class="Bound">x</a> <a id="724" class="Symbol">(</a><a id="725" href="Cubical.Data.Fin.Recursive.Base.html#507" class="Function">elim</a> <a id="730" href="Cubical.Data.Fin.Recursive.Base.html#701" class="Bound">P</a> <a id="732" href="Cubical.Data.Fin.Recursive.Base.html#703" class="Bound">fz</a> <a id="735" href="Cubical.Data.Fin.Recursive.Base.html#706" class="Bound">fs</a> <a id="738" href="Cubical.Data.Fin.Recursive.Base.html#714" class="Bound">x</a><a id="739" class="Symbol">)</a>

<a id="toℕ"></a><a id="742" href="Cubical.Data.Fin.Recursive.Base.html#742" class="Function">toℕ</a> <a id="746" class="Symbol">:</a> <a id="748" href="Cubical.Data.Fin.Recursive.Base.html#287" class="Function">Fin</a> <a id="752" href="Cubical.Data.Fin.Recursive.Base.html#381" class="Generalizable">k</a> <a id="754" class="Symbol">→</a> <a id="756" href="Agda.Builtin.Nat.html#203" class="Datatype">ℕ</a>
<a id="758" href="Cubical.Data.Fin.Recursive.Base.html#742" class="Function">toℕ</a> <a id="762" class="Symbol">{</a><a id="763" href="Agda.Builtin.Nat.html#234" class="InductiveConstructor">suc</a> <a id="767" href="Cubical.Data.Fin.Recursive.Base.html#767" class="Bound">k</a><a id="768" class="Symbol">}</a> <a id="772" href="Cubical.Data.Fin.Recursive.Base.html#253" class="InductiveConstructor">zero</a> <a id="778" class="Symbol">=</a> <a id="780" href="Agda.Builtin.Nat.html#221" class="InductiveConstructor">zero</a>
<a id="785" href="Cubical.Data.Fin.Recursive.Base.html#742" class="Function">toℕ</a> <a id="789" class="Symbol">{</a><a id="790" href="Agda.Builtin.Nat.html#234" class="InductiveConstructor">suc</a> <a id="794" href="Cubical.Data.Fin.Recursive.Base.html#794" class="Bound">k</a><a id="795" class="Symbol">}</a> <a id="797" class="Symbol">(</a><a id="798" href="Cubical.Data.Fin.Recursive.Base.html#269" class="InductiveConstructor">suc</a> <a id="802" href="Cubical.Data.Fin.Recursive.Base.html#802" class="Bound">n</a><a id="803" class="Symbol">)</a> <a id="805" class="Symbol">=</a> <a id="807" href="Agda.Builtin.Nat.html#234" class="InductiveConstructor">suc</a> <a id="811" class="Symbol">(</a><a id="812" href="Cubical.Data.Fin.Recursive.Base.html#742" class="Function">toℕ</a> <a id="816" href="Cubical.Data.Fin.Recursive.Base.html#802" class="Bound">n</a><a id="817" class="Symbol">)</a>
</pre></body></html>
Loading

0 comments on commit 061ff07

Please sign in to comment.