Module headers

Every Agda module should have a module header like

module Modules.Basic where


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


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

In the following slides we will see declarations like