26 lines
2.5 KiB
HTML
26 lines
2.5 KiB
HTML
|
<!DOCTYPE HTML>
|
||
|
|
<html><head><meta charset="utf-8"><title>Data.Empty</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Comment">------------------------------------------------------------------------</a>
|
||
|
|
<a id="74" class="Comment">-- The Agda standard library</a>
|
||
|
|
<a id="103" class="Comment">--</a>
|
||
|
|
<a id="106" class="Comment">-- Empty type</a>
|
||
|
|
<a id="120" class="Comment">------------------------------------------------------------------------</a>
|
||
|
|
|
||
|
|
<a id="194" class="Symbol">{-#</a> <a id="198" class="Keyword">OPTIONS</a> <a id="206" class="Pragma">--without-K</a> <a id="218" class="Pragma">--safe</a> <a id="225" class="Symbol">#-}</a>
|
||
|
|
|
||
|
|
<a id="230" class="Keyword">module</a> <a id="237" href="Data.Empty.html" class="Module">Data.Empty</a> <a id="248" class="Keyword">where</a>
|
||
|
|
|
||
|
|
<a id="255" class="Comment">------------------------------------------------------------------------</a>
|
||
|
|
<a id="328" class="Comment">-- Definition</a>
|
||
|
|
|
||
|
|
<a id="343" class="Comment">-- Note that by default the empty type is not universe polymorphic as it</a>
|
||
|
|
<a id="416" class="Comment">-- often results in unsolved metas. See `Data.Empty.Polymorphic` for a</a>
|
||
|
|
<a id="487" class="Comment">-- universe polymorphic variant.</a>
|
||
|
|
|
||
|
|
<a id="521" class="Keyword">data</a> <a id="⊥"></a><a id="526" href="Data.Empty.html#526" class="Datatype">⊥</a> <a id="528" class="Symbol">:</a> <a id="530" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="534" class="Keyword">where</a>
|
||
|
|
|
||
|
|
<a id="541" class="Comment">------------------------------------------------------------------------</a>
|
||
|
|
<a id="614" class="Comment">-- Functions</a>
|
||
|
|
|
||
|
|
<a id="⊥-elim"></a><a id="628" href="Data.Empty.html#628" class="Function">⊥-elim</a> <a id="635" class="Symbol">:</a> <a id="637" class="Symbol">∀</a> <a id="639" class="Symbol">{</a><a id="640" href="Data.Empty.html#640" class="Bound">w</a><a id="641" class="Symbol">}</a> <a id="643" class="Symbol">{</a><a id="644" href="Data.Empty.html#644" class="Bound">Whatever</a> <a id="653" class="Symbol">:</a> <a id="655" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="659" href="Data.Empty.html#640" class="Bound">w</a><a id="660" class="Symbol">}</a> <a id="662" class="Symbol">→</a> <a id="664" href="Data.Empty.html#526" class="Datatype">⊥</a> <a id="666" class="Symbol">→</a> <a id="668" href="Data.Empty.html#644" class="Bound">Whatever</a>
|
||
|
|
<a id="677" href="Data.Empty.html#628" class="Function">⊥-elim</a> <a id="684" class="Symbol">()</a>
|
||
|
|
</pre></body></html>
|