StructureOfAnAgdaProgram

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

Agda programs are structured as modules. The contents of a module are declarations (which may include submodule declarations). Each Agda source file declares exactly one top-level module whose name matches the filename.

A module exporting a function main : IO a can be compiled to a standalone executable. A tiny example of this, which would be put in a file called "hello.agda":

module hello where
  open import IO
  main = run (putStrLn "Hello, World!")

This uses the IO module in the standard library.