Source Files


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.