-
Notifications
You must be signed in to change notification settings - Fork 0
/
Agda.Builtin.FromNeg.html
19 lines (14 loc) · 4 KB
/
Agda.Builtin.FromNeg.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Agda.Builtin.FromNeg</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-sized-types</a> <a id="49" class="Pragma">--no-guardedness</a>
<a id="78" class="Pragma">--no-subtyping</a> <a id="93" class="Symbol">#-}</a>
<a id="98" class="Keyword">module</a> <a id="105" href="Agda.Builtin.FromNeg.html" class="Module">Agda.Builtin.FromNeg</a> <a id="126" class="Keyword">where</a>
<a id="133" class="Keyword">open</a> <a id="138" class="Keyword">import</a> <a id="145" href="Agda.Primitive.html" class="Module">Agda.Primitive</a>
<a id="160" class="Keyword">open</a> <a id="165" class="Keyword">import</a> <a id="172" href="Agda.Builtin.Nat.html" class="Module">Agda.Builtin.Nat</a>
<a id="190" class="Keyword">record</a> <a id="Negative"></a><a id="197" href="Agda.Builtin.FromNeg.html#197" class="Record">Negative</a> <a id="206" class="Symbol">{</a><a id="207" href="Agda.Builtin.FromNeg.html#207" class="Bound">a</a><a id="208" class="Symbol">}</a> <a id="210" class="Symbol">(</a><a id="211" href="Agda.Builtin.FromNeg.html#211" class="Bound">A</a> <a id="213" class="Symbol">:</a> <a id="215" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="219" href="Agda.Builtin.FromNeg.html#207" class="Bound">a</a><a id="220" class="Symbol">)</a> <a id="222" class="Symbol">:</a> <a id="224" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="228" class="Symbol">(</a><a id="229" href="Agda.Primitive.html#780" class="Primitive">lsuc</a> <a id="234" href="Agda.Builtin.FromNeg.html#207" class="Bound">a</a><a id="235" class="Symbol">)</a> <a id="237" class="Keyword">where</a>
<a id="245" class="Keyword">field</a>
<a id="Negative.Constraint"></a><a id="255" href="Agda.Builtin.FromNeg.html#255" class="Field">Constraint</a> <a id="266" class="Symbol">:</a> <a id="268" href="Agda.Builtin.Nat.html#192" class="Datatype">Nat</a> <a id="272" class="Symbol">→</a> <a id="274" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="278" href="Agda.Builtin.FromNeg.html#207" class="Bound">a</a>
<a id="Negative.fromNeg"></a><a id="284" href="Agda.Builtin.FromNeg.html#284" class="Field">fromNeg</a> <a id="292" class="Symbol">:</a> <a id="294" class="Symbol">∀</a> <a id="296" href="Agda.Builtin.FromNeg.html#296" class="Bound">n</a> <a id="298" class="Symbol">→</a> <a id="300" class="Symbol">{{</a><a id="302" href="Agda.Builtin.FromNeg.html#302" class="Bound">_</a> <a id="304" class="Symbol">:</a> <a id="306" href="Agda.Builtin.FromNeg.html#255" class="Field">Constraint</a> <a id="317" href="Agda.Builtin.FromNeg.html#296" class="Bound">n</a><a id="318" class="Symbol">}}</a> <a id="321" class="Symbol">→</a> <a id="323" href="Agda.Builtin.FromNeg.html#211" class="Bound">A</a>
<a id="326" class="Keyword">open</a> <a id="331" href="Agda.Builtin.FromNeg.html#197" class="Module">Negative</a> <a id="340" class="Symbol">{{...}}</a> <a id="348" class="Keyword">public</a> <a id="355" class="Keyword">using</a> <a id="361" class="Symbol">(</a><a id="362" href="Agda.Builtin.FromNeg.html#284" class="Field">fromNeg</a><a id="369" class="Symbol">)</a>
<a id="372" class="Symbol">{-#</a> <a id="376" class="Keyword">BUILTIN</a> <a id="384" class="Keyword">FROMNEG</a> <a id="392" href="Agda.Builtin.FromNeg.html#284" class="Field">fromNeg</a> <a id="400" class="Symbol">#-}</a>
<a id="404" class="Symbol">{-#</a> <a id="408" class="Keyword">DISPLAY</a> <a id="416" href="Agda.Builtin.FromNeg.html#284" class="Field">Negative.fromNeg</a> <a id="433" class="Pragma">_</a> <a id="435" href="Agda.Builtin.FromNeg.html#435" class="Bound">n</a> <a id="437" class="Pragma">=</a> <a id="439" href="Agda.Builtin.FromNeg.html#284" class="Field">fromNeg</a> <a id="447" href="Agda.Builtin.FromNeg.html#435" class="Bound">n</a> <a id="449" class="Symbol">#-}</a>
</pre></body></html>