Comments

See the official user manual for the most up-to-date version of the information on this page.

TOC

Agda has both single-line and multi-line comments.

A single-line comment is two hyphens followed by a sequence of any characters except newline. The comment ends with a newline.

A multi-line comment is any sequence of characters delimited by {- and -}. Multi-line comments may be nested, and must be nested properly. Comments may not appear in string literals. (Apparent comments in string literals are part of the string.)

Example:

{-
  Here is a comment above a module.
-}
module Comments where --this is a comment! --fooo@.. jjwjw
  open import Data.Bool
  open import Data.String
  not-comment : Bool -> Set
{- but this is OK {-
                    and indeed -}
 they can be nested -}
  s : String
  s = "{- This is not a comment {- Notice the bad nesting -}"
  not-comment b = {- another comment -} ? --more end-of-line