Layout

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:
    λ { p1 → t1 ; ... ; pn -> tn }
  • records:
    record { x1 = t1 ; ... ; xn = tn }