Contents Previous Next

Naming conventions

Files and modules

The namespace or package equivalent in Agda, called a module, appears at the beginning of every file:

module Lang.naming where

Filenames and module headers are required to match according the the following pattern: the supported filenames that can contain the module named intro are:

This file is written in markdown and hence we use the name

Literate programming

The last three file extensions above are part of what’s called “literate programming” wherein one can write markdown or latex documents with agda code surrounded in code blocks marked agda, similar to how this page itself is written!


The Agda compiler can then validate the agda code inside the agda code blocks, thus guaranteeing the correctness of the math in the documents.

Other material

There are a host of other high quality material on the web, though all of them might not be beginner friendly. They are listed in Agda’s official documentation. We flick some stuff from many of them and water them down for novices here.

Data Structures