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.