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


Agda code is written in plain text files consisting of Unicode characters encoded in UTF-8.

The tokens that may appear in source files are literals, names, and keywords. Tokens are separated by whitespace, including comments, and organised into blocks.

Agda programs are organised into modules, with one top-level module per file.

Page last modified on December 14, 2018, at 06:47 PM
Powered by PmWiki