Layout

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

TOC

Agda code is structured in blocks which have the form

  <keyword> <args> { <block> ; <block> ; ... }

Instead of writing braces and semicolons, one can use layout, that is, newlines and indentation, to delimit blocks and separate their components.

In general

  <b1> { <b2> { <b3> ; ... } ; <b4> ; ... }

is equivalent to

  <b1>
    <b2>
      <b3>
      ...
    <b4>
    ...

However, layout cannot be used with:

• pattern matching lambda abstractions:
  λ { p₁ → t₁ ; ... ; p_n -> t_n }
• records:
  record { x₁ = t₁ ; ... ; x_n = t_n }