caryoscelus
/
agda


			
							1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950
							<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>MdMultiLanguage</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Background">&lt;!--
</a><a id="6" class="Markup">```
</a><a id="10" class="Keyword">module</a> <a id="17" href="MdMultiLanguage.html" class="Module">MdMultiLanguage</a> <a id="33" class="Keyword">where</a>
<a id="39" class="Markup">```
</a><a id="43" class="Background">--&gt;

  ```haskell
a :: Bool
a = True
```

     </a><a id="90" class="Markup">```
</a><a id="94" class="Keyword">data</a> <a id="Bool"></a><a id="99" href="MdMultiLanguage.html#99" class="Datatype">Bool</a> <a id="104" class="Symbol">:</a> <a id="106" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="110" class="Keyword">where</a>
    <a id="Bool.true"></a><a id="120" href="MdMultiLanguage.html#120" class="InductiveConstructor">true</a> <a id="125" class="Symbol">:</a> <a id="127" href="MdMultiLanguage.html#99" class="Datatype">Bool</a>
    <a id="Bool.false"></a><a id="136" href="MdMultiLanguage.html#136" class="InductiveConstructor">false</a> <a id="142" class="Symbol">:</a> <a id="144" href="MdMultiLanguage.html#99" class="Datatype">Bool</a>
    <a id="Bool.aa"></a><a id="153" href="MdMultiLanguage.html#153" class="InductiveConstructor">aa</a> <a id="156" class="Symbol">:</a> <a id="158" class="Comment">{- ``` -}</a> <a id="168" href="MdMultiLanguage.html#99" class="Datatype">Bool</a>

<a id="a"></a><a id="174" href="MdMultiLanguage.html#174" class="Function">a</a> <a id="176" class="Symbol">:</a> <a id="178" href="MdMultiLanguage.html#99" class="Datatype">Bool</a>
<a id="183" href="MdMultiLanguage.html#174" class="Function">a</a> <a id="185" class="Symbol">=</a> <a id="187" href="MdMultiLanguage.html#120" class="InductiveConstructor">true</a>

<a id="193" class="Markup">```
</a><a id="197" class="Background">
This is also parsed:

</a><a id="220" class="Markup">```agda
</a>  <a id="230" class="Keyword">module</a> <a id="MdQuotedDelim"></a><a id="237" href="MdMultiLanguage.html#237" class="Module">MdQuotedDelim</a> <a id="251" class="Keyword">where</a>

        <a id="266" class="Keyword">data</a> <a id="MdQuotedDelim.Bool’"></a><a id="271" href="MdMultiLanguage.html#271" class="Datatype">Bool’</a> <a id="277" class="Symbol">:</a> <a id="279" href="Agda.Primitive.html#311" class="Primitive">Set</a> <a id="283" class="Keyword">where</a>
            <a id="MdQuotedDelim.Bool’.true"></a><a id="301" href="MdMultiLanguage.html#301" class="InductiveConstructor">true</a> <a id="306" class="Symbol">:</a> <a id="308" href="MdMultiLanguage.html#271" class="Datatype">Bool’</a>
            <a id="MdQuotedDelim.Bool’.false"></a><a id="326" href="MdMultiLanguage.html#326" class="InductiveConstructor">false</a> <a id="332" class="Symbol">:</a> <a id="334" href="MdMultiLanguage.html#271" class="Datatype">Bool’</a>
            <a id="MdQuotedDelim.Bool’.aa"></a><a id="352" href="MdMultiLanguage.html#352" class="InductiveConstructor">aa</a> <a id="355" class="Symbol">:</a> <a id="357" class="Comment">{- ``` -}</a> <a id="367" href="MdMultiLanguage.html#271" class="Datatype">Bool’</a>

        <a id="MdQuotedDelim.a’"></a><a id="382" href="MdMultiLanguage.html#382" class="Function">a’</a> <a id="385" class="Symbol">:</a> <a id="387" href="MdMultiLanguage.html#271" class="Datatype">Bool’</a>
        <a id="401" href="MdMultiLanguage.html#382" class="Function">a’</a> <a id="404" class="Symbol">=</a> <a id="406" href="MdMultiLanguage.html#352" class="InductiveConstructor">aa</a>
<a id="409" class="Markup">  ```
</a><a id="415" class="Background">
* This one is not:

    a : Set
    a = false


* But this one is:

  </a><a id="486" class="Markup">```
</a><a id="b"></a><a id="490" href="MdMultiLanguage.html#490" class="Function">b</a> <a id="492" class="Symbol">:</a> <a id="494" href="MdMultiLanguage.html#99" class="Datatype">Bool</a>
<a id="499" href="MdMultiLanguage.html#490" class="Function">b</a> <a id="501" class="Symbol">=</a> <a id="503" href="MdMultiLanguage.html#136" class="InductiveConstructor">false</a>
<a id="509" class="Markup"> ```
</a></pre></body></html>