-
Notifications
You must be signed in to change notification settings - Fork 9
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
20 changed files
with
1,027 additions
and
984 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,32 @@ | ||
| <!DOCTYPE HTML> | ||
| <html><head><meta charset="utf-8"><title>Data.Singleton</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">--without-K</a> <a id="25" class="Pragma">--safe</a> <a id="32" class="Symbol">#-}</a> | ||
|
|
||
| <a id="37" class="Keyword">module</a> <a id="44" href="Data.Singleton.html" class="Module">Data.Singleton</a> <a id="59" class="Keyword">where</a> | ||
|
|
||
| <a id="66" class="Keyword">open</a> <a id="71" class="Keyword">import</a> <a id="78" href="Level.html" class="Module">Level</a> <a id="84" class="Keyword">using</a> <a id="90" class="Symbol">(</a><a id="91" href="Agda.Primitive.html#597" class="Postulate">Level</a><a id="96" class="Symbol">;</a> <a id="98" href="Level.html#534" class="Function">levelOfType</a><a id="109" class="Symbol">)</a> | ||
| <a id="111" class="Keyword">open</a> <a id="116" class="Keyword">import</a> <a id="123" href="Data.Empty.Polymorphic.html" class="Module">Data.Empty.Polymorphic</a> <a id="146" class="Keyword">using</a> <a id="152" class="Symbol">(</a><a id="153" href="Data.Empty.Polymorphic.html#331" class="Function">⊥</a><a id="154" class="Symbol">)</a> | ||
| <a id="156" class="Keyword">open</a> <a id="161" class="Keyword">import</a> <a id="168" href="Data.Maybe.Base.html" class="Module">Data.Maybe.Base</a> <a id="184" class="Keyword">using</a> <a id="190" class="Symbol">(</a><a id="191" href="Agda.Builtin.Maybe.html#136" class="Datatype">Maybe</a><a id="196" class="Symbol">;</a> <a id="198" href="Agda.Builtin.Maybe.html#195" class="InductiveConstructor">nothing</a><a id="205" class="Symbol">;</a> <a id="207" href="Agda.Builtin.Maybe.html#174" class="InductiveConstructor">just</a><a id="211" class="Symbol">)</a> | ||
| <a id="213" class="Keyword">open</a> <a id="218" class="Keyword">import</a> <a id="225" href="Data.Sum.Base.html" class="Module">Data.Sum.Base</a> <a id="239" class="Keyword">using</a> <a id="245" class="Symbol">(</a><a id="246" href="Data.Sum.Base.html#734" class="Datatype Operator">_⊎_</a><a id="249" class="Symbol">;</a> <a id="251" href="Data.Sum.Base.html#784" class="InductiveConstructor">inj₁</a><a id="255" class="Symbol">;</a> <a id="257" href="Data.Sum.Base.html#809" class="InductiveConstructor">inj₂</a><a id="261" class="Symbol">)</a> | ||
|
|
||
| <a id="264" class="Keyword">private</a> | ||
| <a id="274" class="Keyword">variable</a> | ||
| <a id="287" href="Data.Singleton.html#287" class="Generalizable">a</a> <a id="289" href="Data.Singleton.html#289" class="Generalizable">b</a> <a id="291" class="Symbol">:</a> <a id="293" href="Agda.Primitive.html#597" class="Postulate">Level</a> | ||
| <a id="303" href="Data.Singleton.html#303" class="Generalizable">A</a> <a id="305" class="Symbol">:</a> <a id="307" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="311" href="Data.Singleton.html#287" class="Generalizable">a</a> | ||
| <a id="317" href="Data.Singleton.html#317" class="Generalizable">B</a> <a id="319" class="Symbol">:</a> <a id="321" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="325" href="Data.Singleton.html#289" class="Generalizable">b</a> | ||
|
|
||
| <a id="328" class="Keyword">infix</a> <a id="334" class="Number">0</a> <a id="336" href="Data.Singleton.html#386" class="InductiveConstructor Operator">_!</a> | ||
| <a id="339" class="Keyword">data</a> <a id="Singleton"></a><a id="344" href="Data.Singleton.html#344" class="Datatype">Singleton</a> <a id="354" class="Symbol">{</a><a id="355" href="Data.Singleton.html#355" class="Bound">A</a> <a id="357" class="Symbol">:</a> <a id="359" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="363" href="Data.Singleton.html#287" class="Generalizable">a</a><a id="364" class="Symbol">}</a> <a id="366" class="Symbol">:</a> <a id="368" href="Data.Singleton.html#355" class="Bound">A</a> <a id="370" class="Symbol">→</a> <a id="372" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="376" href="Data.Singleton.html#363" class="Bound">a</a> <a id="378" class="Keyword">where</a> | ||
| <a id="Singleton._!"></a><a id="386" href="Data.Singleton.html#386" class="InductiveConstructor Operator">_!</a> <a id="389" class="Symbol">:</a> <a id="391" class="Symbol">(</a><a id="392" href="Data.Singleton.html#392" class="Bound">a</a> <a id="394" class="Symbol">:</a> <a id="396" href="Data.Singleton.html#355" class="Bound">A</a><a id="397" class="Symbol">)</a> <a id="399" class="Symbol">→</a> <a id="401" href="Data.Singleton.html#344" class="Datatype">Singleton</a> <a id="411" href="Data.Singleton.html#392" class="Bound">a</a> | ||
|
|
||
| <a id="fromJust"></a><a id="414" href="Data.Singleton.html#414" class="Function">fromJust</a> <a id="423" class="Symbol">:</a> <a id="425" href="Agda.Builtin.Maybe.html#136" class="Datatype">Maybe</a> <a id="431" href="Data.Singleton.html#303" class="Generalizable">A</a> <a id="433" class="Symbol">→</a> <a id="435" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="439" class="Symbol">(</a><a id="440" href="Level.html#534" class="Function">levelOfType</a> <a id="452" href="Data.Singleton.html#303" class="Generalizable">A</a><a id="453" class="Symbol">)</a> | ||
| <a id="455" href="Data.Singleton.html#414" class="Function">fromJust</a> <a id="464" class="Symbol">(</a><a id="465" href="Agda.Builtin.Maybe.html#174" class="InductiveConstructor">just</a> <a id="470" href="Data.Singleton.html#470" class="Bound">a</a><a id="471" class="Symbol">)</a> <a id="473" class="Symbol">=</a> <a id="475" href="Data.Singleton.html#344" class="Datatype">Singleton</a> <a id="485" href="Data.Singleton.html#470" class="Bound">a</a> | ||
| <a id="487" href="Data.Singleton.html#414" class="Function">fromJust</a> <a id="496" href="Agda.Builtin.Maybe.html#195" class="InductiveConstructor">nothing</a> <a id="505" class="Symbol">=</a> <a id="507" href="Data.Empty.Polymorphic.html#331" class="Function">⊥</a> | ||
|
|
||
| <a id="fromInj₁"></a><a id="510" href="Data.Singleton.html#510" class="Function">fromInj₁</a> <a id="519" class="Symbol">:</a> <a id="521" href="Data.Singleton.html#303" class="Generalizable">A</a> <a id="523" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="525" href="Data.Singleton.html#317" class="Generalizable">B</a> <a id="527" class="Symbol">→</a> <a id="529" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="533" class="Symbol">(</a><a id="534" href="Level.html#534" class="Function">levelOfType</a> <a id="546" href="Data.Singleton.html#303" class="Generalizable">A</a><a id="547" class="Symbol">)</a> | ||
| <a id="549" href="Data.Singleton.html#510" class="Function">fromInj₁</a> <a id="558" class="Symbol">(</a><a id="559" href="Data.Sum.Base.html#784" class="InductiveConstructor">inj₁</a> <a id="564" href="Data.Singleton.html#564" class="Bound">a</a><a id="565" class="Symbol">)</a> <a id="567" class="Symbol">=</a> <a id="569" href="Data.Singleton.html#344" class="Datatype">Singleton</a> <a id="579" href="Data.Singleton.html#564" class="Bound">a</a> | ||
| <a id="581" href="Data.Singleton.html#510" class="Function">fromInj₁</a> <a id="590" class="Symbol">(</a><a id="591" href="Data.Sum.Base.html#809" class="InductiveConstructor">inj₂</a> <a id="596" class="Symbol">_)</a> <a id="599" class="Symbol">=</a> <a id="601" href="Data.Empty.Polymorphic.html#331" class="Function">⊥</a> | ||
|
|
||
| <a id="fromInj₂"></a><a id="604" href="Data.Singleton.html#604" class="Function">fromInj₂</a> <a id="613" class="Symbol">:</a> <a id="615" href="Data.Singleton.html#303" class="Generalizable">A</a> <a id="617" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="619" href="Data.Singleton.html#317" class="Generalizable">B</a> <a id="621" class="Symbol">→</a> <a id="623" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="627" class="Symbol">(</a><a id="628" href="Level.html#534" class="Function">levelOfType</a> <a id="640" href="Data.Singleton.html#317" class="Generalizable">B</a><a id="641" class="Symbol">)</a> | ||
| <a id="643" href="Data.Singleton.html#604" class="Function">fromInj₂</a> <a id="652" class="Symbol">(</a><a id="653" href="Data.Sum.Base.html#784" class="InductiveConstructor">inj₁</a> <a id="658" class="Symbol">_)</a> <a id="661" class="Symbol">=</a> <a id="663" href="Data.Empty.Polymorphic.html#331" class="Function">⊥</a> | ||
| <a id="665" href="Data.Singleton.html#604" class="Function">fromInj₂</a> <a id="674" class="Symbol">(</a><a id="675" href="Data.Sum.Base.html#809" class="InductiveConstructor">inj₂</a> <a id="680" href="Data.Singleton.html#680" class="Bound">b</a><a id="681" class="Symbol">)</a> <a id="683" class="Symbol">=</a> <a id="685" href="Data.Singleton.html#344" class="Datatype">Singleton</a> <a id="695" href="Data.Singleton.html#680" class="Bound">b</a> | ||
| </pre></body></html> |
This file was deleted.
Oops, something went wrong.
Oops, something went wrong.