See the official user manual for the most up-to-date version of the information on this page.
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
Page last modified on December 14, 2018, at 03:39 pm
Powered by
PmWiki