Test.Space.Markdown

module Test.Space.Markdown
  where         -- this line is indented 2 spaces
module _ where  -- this line is not indented

The above code block starts on the first line, and is followed by a blank line.

The following code block is not preceded by a blank line.

-- Agda does not require blank lines around code blocks.

It is also not followed by a blank line.

The following code block is preceded by a blank line, which is ignored in Markdown.

-- Agda allows blank lines around code blocks

It is followed by a blank line, which is ignored in Markdown.

Blank lines inside code blocks are preserved:

-- This code line has blank lines around it.

Agda does not generate any Markdown for completely empty code blocks.

The following empty-looking code block has multiple newlines and spaces:

They are preserved.

Agda code can be indented:

  -- This comment is indented 2 spaces.

  module _
    where
    -- This comment is indented 4 spaces.

-- This comment is not indented.

The code block itself can be indented:

  -- This indented comment is in an indented code block.