blob: 5829754e4ea56efc9736463cdddf1efab4669345 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
|
<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Agda.Primitive</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Comment">-- The Agda primitives (preloaded).</a>
<a id="38" class="Symbol">{-#</a> <a id="42" class="Keyword">OPTIONS</a> <a id="50" class="Pragma">--without-K</a> <a id="62" class="Pragma">--no-subtyping</a> <a id="77" class="Symbol">#-}</a>
<a id="82" class="Keyword">module</a> <a id="89" href="Agda.Primitive.html" class="Module">Agda.Primitive</a> <a id="104" class="Keyword">where</a>
<a id="111" class="Comment">------------------------------------------------------------------------</a>
<a id="184" class="Comment">-- Universe levels</a>
<a id="203" class="Comment">------------------------------------------------------------------------</a>
<a id="277" class="Keyword">infixl</a> <a id="284" class="Number">6</a> <a id="286" href="Agda.Primitive.html#636" class="Primitive Operator">_⊔_</a>
<a id="291" class="Comment">-- Level is the first thing we need to define.</a>
<a id="338" class="Comment">-- The other postulates can only be checked if built-in Level is known.</a>
<a id="411" class="Keyword">postulate</a>
<a id="Level"></a><a id="423" href="Agda.Primitive.html#423" class="Postulate">Level</a> <a id="429" class="Symbol">:</a> <a id="431" class="PrimitiveType">Set</a>
<a id="436" class="Comment">-- MAlonzo compiles Level to (). This should be safe, because it is</a>
<a id="504" class="Comment">-- not possible to pattern match on levels.</a>
<a id="549" class="Symbol">{-#</a> <a id="553" class="Keyword">BUILTIN</a> <a id="561" class="Keyword">LEVEL</a> <a id="567" href="Agda.Primitive.html#423" class="Postulate">Level</a> <a id="573" class="Symbol">#-}</a>
<a id="578" class="Keyword">postulate</a>
<a id="lzero"></a><a id="590" href="Agda.Primitive.html#590" class="Postulate">lzero</a> <a id="596" class="Symbol">:</a> <a id="598" href="Agda.Primitive.html#423" class="Postulate">Level</a>
<a id="lsuc"></a><a id="606" href="Agda.Primitive.html#606" class="Postulate">lsuc</a> <a id="612" class="Symbol">:</a> <a id="614" class="Symbol">(</a><a id="615" href="Agda.Primitive.html#615" class="Bound">ℓ</a> <a id="617" class="Symbol">:</a> <a id="619" href="Agda.Primitive.html#423" class="Postulate">Level</a><a id="624" class="Symbol">)</a> <a id="626" class="Symbol">→</a> <a id="628" href="Agda.Primitive.html#423" class="Postulate">Level</a>
<a id="_⊔_"></a><a id="636" href="Agda.Primitive.html#636" class="Postulate Operator">_⊔_</a> <a id="642" class="Symbol">:</a> <a id="644" class="Symbol">(</a><a id="645" href="Agda.Primitive.html#645" class="Bound">ℓ₁</a> <a id="648" href="Agda.Primitive.html#648" class="Bound">ℓ₂</a> <a id="651" class="Symbol">:</a> <a id="653" href="Agda.Primitive.html#423" class="Postulate">Level</a><a id="658" class="Symbol">)</a> <a id="660" class="Symbol">→</a> <a id="662" href="Agda.Primitive.html#423" class="Postulate">Level</a>
<a id="669" class="Symbol">{-#</a> <a id="673" class="Keyword">BUILTIN</a> <a id="681" class="Keyword">LEVELZERO</a> <a id="691" href="Agda.Primitive.html#590" class="Primitive">lzero</a> <a id="697" class="Symbol">#-}</a>
<a id="701" class="Symbol">{-#</a> <a id="705" class="Keyword">BUILTIN</a> <a id="713" class="Keyword">LEVELSUC</a> <a id="723" href="Agda.Primitive.html#606" class="Primitive">lsuc</a> <a id="729" class="Symbol">#-}</a>
<a id="733" class="Symbol">{-#</a> <a id="737" class="Keyword">BUILTIN</a> <a id="745" class="Keyword">LEVELMAX</a> <a id="755" href="Agda.Primitive.html#636" class="Primitive Operator">_⊔_</a> <a id="761" class="Symbol">#-}</a>
<a id="766" class="Symbol">{-#</a> <a id="770" class="Keyword">BUILTIN</a> <a id="778" class="Keyword">SETOMEGA</a> <a id="Setω"></a><a id="787" href="Agda.Primitive.html#787" class="Primitive">Setω</a> <a id="792" class="Symbol">#-}</a>
</pre></body></html>
|