<div dir="ltr"><div>Hi Marko,</div><div><br></div><div>I believe the literal Agda mode *only* looks at the parts between the begin- and end-code markers (in this case ```). This includes begin- and end-comment markers, so in this case they are ignored. One trick you could use is to put some text immediately after the first triple backtick, which will cause Agda to ignore the whole block. E.g.</div><div><br></div><div>```ignore<br>
count : ∀ {Γ} → (n : ℕ) → (p : n < length Γ) → Γ ∋ lookup Γ n p<br>
count {_ , _} zero _     =  Z<br>
count {Γ , _} (suc n) (s≤s p)  =  S (count n p)<br>
```</div><div><br></div><div>Hope that helps!</div><div><br></div><div>-- Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Sep 11, 2020 at 8:51 AM Marko Dimjašević <<a href="mailto:marko@dimjasevic.net">marko@dimjasevic.net</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Dear all,<br>
<br>
Is it possible to write multi-line comments in literate Agda files? I have<br>
a file with a .lagda.md filename extension loaded in the Agda Emacs mode<br>
(defined in 'agda2-mode.el'). I'm making some changes to the code in it and<br>
because type-checking takes so much time (when loading a file with C-c C-<br>
l), I'd like to comment out the part of the file below my changes such that<br>
I don't waste time on type-checking definitions that are not affecting my<br>
changes.<br>
<br>
I attempted to comment out that part of the file by enclosing it in {- and<br>
-}, however, that doesn't comment it out. It looks like the first code<br>
block nullifies the opening multi-line comment delimiter. For example, in<br>
the following snippet:<br>
<br>
{-<br>
Given the above, we can convert a natural to a corresponding<br>
de Bruijn index, looking up its type in the context:<br>
```<br>
count : ∀ {Γ} → (n : ℕ) → (p : n < length Γ) → Γ ∋ lookup Γ n p<br>
count {_ , _} zero _     =  Z<br>
count {Γ , _} (suc n) (s≤s p)  =  S (count n p)<br>
```<br>
-}<br>
<br>
<br>
the part that start the code block, i.e. ```, ends the comment span and<br>
start a code block that gets type-checked.<br>
<br>
Is this a bug or a feature?<br>
<br>
Should I be writing multi-line comments in literate Agda files in some<br>
other way?<br>
<br>
<br>
-- <br>
Regards,<br>
Marko Dimjašević <<a href="mailto:marko@dimjasevic.net" target="_blank">marko@dimjasevic.net</a>><br>
<a href="https://dimjasevic.net/marko" rel="noreferrer" target="_blank">https://dimjasevic.net/marko</a><br>
Mastodon: <a href="https://mamot.fr/@mdimjasevic" rel="noreferrer" target="_blank">https://mamot.fr/@mdimjasevic</a><br>
PGP key ID:       056E61A6F3B6C9323049DBF9565EE9641503F0AA<br>
Learn email self-defense! <a href="https://emailselfdefense.fsf.org" rel="noreferrer" target="_blank">https://emailselfdefense.fsf.org</a><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>