deploy: afb5392

_sources/features.md.txt

@@ -299,7 +299,7 @@ five = (id :: Natural -> Natural) 5
 (0-Quantity)=
 ## 0-Quantity Parameters
 
-Parameters can be annotated with a _quantity_ of either `0` or `ω` (the default quantity is `ω` if no quantity is explicitly annotated). Such parameters are irrelevant to evaluation, so they are irrelevant to the compiled Haskell program, and so agda2hs erases them.
+Parameters can be annotated with a _quantity_ of either `0` or `ω` (the default quantity is `ω` if no quantity is explicitly annotated). Parameters annotated with `0` are irrelevant to evaluation, so they are irrelevant to the compiled Haskell program, and so agda2hs erases them.
 
 Agda:
 ```agda

features.html

@@ -391,7 +391,7 @@ <h2>Explicit type singatures<a class="headerlink" href="#explicit-type-singature
 </section>
 <section id="quantity-parameters">
 <span id="quantity"></span><h2>0-Quantity Parameters<a class="headerlink" href="#quantity-parameters" title="Permalink to this heading"></a></h2>
-<p>Parameters can be annotated with a <em>quantity</em> of either <code class="docutils literal notranslate"><span class="pre">0</span></code> or <code class="docutils literal notranslate"><span class="pre">ω</span></code> (the default quantity is <code class="docutils literal notranslate"><span class="pre">ω</span></code> if no quantity is explicitly annotated). Such parameters are irrelevant to evaluation, so they are irrelevant to the compiled Haskell program, and so agda2hs erases them.</p>
+<p>Parameters can be annotated with a <em>quantity</em> of either <code class="docutils literal notranslate"><span class="pre">0</span></code> or <code class="docutils literal notranslate"><span class="pre">ω</span></code> (the default quantity is <code class="docutils literal notranslate"><span class="pre">ω</span></code> if no quantity is explicitly annotated). Parameters annotated with <code class="docutils literal notranslate"><span class="pre">0</span></code> are irrelevant to evaluation, so they are irrelevant to the compiled Haskell program, and so agda2hs erases them.</p>
 <p>Agda:</p>
 <div class="highlight-agda notranslate"><div class="highlight"><pre><span></span><span class="kr">data</span><span class="w"> </span>GhostInt<span class="w"> </span><span class="ow">:</span><span class="w"> </span><span class="kt">Set</span><span class="w"> </span><span class="kr">where</span>
 <span class="w">    </span><span class="nf">MakeGhostInt</span><span class="w"> </span><span class="ow">:</span><span class="w"> </span>@0<span class="w"> </span>Int<span class="w"> </span><span class="ow">→</span><span class="w"> </span>GhostInt