12 lines
1.7 KiB
HTML
12 lines
1.7 KiB
HTML
<!DOCTYPE HTML>
|
||
<html><head><meta charset="utf-8"><title>Agda.Builtin.Unit</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="Pragma">--no-universe-polymorphism</a>
|
||
<a id="71" class="Pragma">--no-sized-types</a> <a id="88" class="Pragma">--no-guardedness</a> <a id="105" class="Pragma">--no-subtyping</a> <a id="120" class="Symbol">#-}</a>
|
||
|
||
<a id="125" class="Keyword">module</a> <a id="132" href="Agda.Builtin.Unit.html" class="Module">Agda.Builtin.Unit</a> <a id="150" class="Keyword">where</a>
|
||
|
||
<a id="157" class="Keyword">record</a> <a id="⊤"></a><a id="164" href="Agda.Builtin.Unit.html#164" class="Record">⊤</a> <a id="166" class="Symbol">:</a> <a id="168" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="172" class="Keyword">where</a>
|
||
<a id="180" class="Keyword">instance</a> <a id="189" class="Keyword">constructor</a> <a id="tt"></a><a id="201" href="Agda.Builtin.Unit.html#201" class="InductiveConstructor">tt</a>
|
||
|
||
<a id="205" class="Symbol">{-#</a> <a id="209" class="Keyword">BUILTIN</a> <a id="217" class="Keyword">UNIT</a> <a id="222" href="Agda.Builtin.Unit.html#164" class="Record">⊤</a> <a id="224" class="Symbol">#-}</a>
|
||
<a id="228" class="Symbol">{-#</a> <a id="232" class="Keyword">COMPILE</a> <a id="240" class="Keyword">GHC</a> <a id="244" href="Agda.Builtin.Unit.html#164" class="Record">⊤</a> <a id="246" class="Pragma">=</a> <a id="248" class="Pragma">data</a> <a id="253" class="Pragma">()</a> <a id="256" class="Pragma">(())</a> <a id="261" class="Symbol">#-}</a>
|
||
</pre></body></html> |