[Agda] Multi-line comments in literate Agda files

[Marko Dimjašević]

Dear all,

Is it possible to write multi-line comments in literate Agda files? I have
a file with a .lagda.md filename extension loaded in the Agda Emacs mode
(defined in 'agda2-mode.el'). I'm making some changes to the code in it and
because type-checking takes so much time (when loading a file with C-c C-
l), I'd like to comment out the part of the file below my changes such that
I don't waste time on type-checking definitions that are not affecting my
changes.

I attempted to comment out that part of the file by enclosing it in {- and
-}, however, that doesn't comment it out. It looks like the first code
block nullifies the opening multi-line comment delimiter. For example, in
the following snippet:

{-
Given the above, we can convert a natural to a corresponding
de Bruijn index, looking up its type in the context:
```
count : ∀ {Γ} → (n : ℕ) → (p : n < length Γ) → Γ ∋ lookup Γ n p
count {_ , _} zero _     =  Z
count {Γ , _} (suc n) (s≤s p)  =  S (count n p)
```
-}


the part that start the code block, i.e. ```, ends the comment span and
start a code block that gets type-checked.

Is this a bug or a feature?

Should I be writing multi-line comments in literate Agda files in some
other way?


-- 
Regards,
Marko Dimjašević <marko at dimjasevic.net>
https://dimjasevic.net/marko
Mastodon: https://mamot.fr/@mdimjasevic
PGP key ID:       056E61A6F3B6C9323049DBF9565EE9641503F0AA
Learn email self-defense! https://emailselfdefense.fsf.org
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: This is a digitally signed message part
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200911/c2314efe/attachment.sig>