16 lines
2.1 KiB
HTML
16 lines
2.1 KiB
HTML
|
<!DOCTYPE HTML>
|
||
|
|
<html><head><meta charset="utf-8"><title>Data.Empty.Irrelevant</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">-- An irrelevant version of ⊥-elim</a>
|
||
|
|
<a id="141" class="Comment">------------------------------------------------------------------------</a>
|
||
|
|
|
||
|
|
<a id="215" class="Symbol">{-#</a> <a id="219" class="Keyword">OPTIONS</a> <a id="227" class="Pragma">--without-K</a> <a id="239" class="Pragma">--safe</a> <a id="246" class="Symbol">#-}</a>
|
||
|
|
|
||
|
|
<a id="251" class="Keyword">module</a> <a id="258" href="Data.Empty.Irrelevant.html" class="Module">Data.Empty.Irrelevant</a> <a id="280" class="Keyword">where</a>
|
||
|
|
|
||
|
|
<a id="287" class="Keyword">open</a> <a id="292" class="Keyword">import</a> <a id="299" href="Data.Empty.html" class="Module">Data.Empty</a> <a id="310" class="Keyword">hiding</a> <a id="317" class="Symbol">(</a><a id="318" href="Data.Empty.html#628" class="Function">⊥-elim</a><a id="324" class="Symbol">)</a>
|
||
|
|
|
||
|
|
<a id="⊥-elim"></a><a id="327" href="Data.Empty.Irrelevant.html#327" class="Function">⊥-elim</a> <a id="334" class="Symbol">:</a> <a id="336" class="Symbol">∀</a> <a id="338" class="Symbol">{</a><a id="339" href="Data.Empty.Irrelevant.html#339" class="Bound">w</a><a id="340" class="Symbol">}</a> <a id="342" class="Symbol">{</a><a id="343" href="Data.Empty.Irrelevant.html#343" class="Bound">Whatever</a> <a id="352" class="Symbol">:</a> <a id="354" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="358" href="Data.Empty.Irrelevant.html#339" class="Bound">w</a><a id="359" class="Symbol">}</a> <a id="361" class="Symbol">→</a> <a id="363" class="Symbol">.</a><a id="364" href="Data.Empty.html#526" class="Datatype">⊥</a> <a id="366" class="Symbol">→</a> <a id="368" href="Data.Empty.Irrelevant.html#343" class="Bound">Whatever</a>
|
||
|
|
<a id="377" href="Data.Empty.Irrelevant.html#327" class="Function">⊥-elim</a> <a id="384" class="Symbol">()</a>
|
||
|
|
</pre></body></html>
|