Module headers

Every Agda module should have a module header like as follows:


module Modules.Basic where

Note that:

Exercise

  1. Install the Agda compiler.
  2. Open a file called First.agda (or something similar) in Emacs.
  3. Fill in the module header.
  4. Load the module to get syntax highlighting.

Declarations

An Agda module is a module header and a list of declarations.

In the following slides we will see declarations like