[Agda] Multi-line comments in literate Agda files

Roman effectfully at gmail.com
Sat Sep 12 13:13:33 CEST 2020


> Uma, thank you for your suggestion! What Nils proposed requires less typing
from me, so I'll go with his proposal.

You can type C-c C-x M-; and that will comment out everything below
the line you're at (including the line).


More information about the Agda mailing list