Test.Space.LaTeX

module Test.Space.LaTeX
  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.

-- Agda allows blank lines around code blocks

It is also followed by a blank line.

Blank lines inside code blocks are preserved:


-- This code line has blank lines around it.


The following code block is completely empty:


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.