Version 2.0.0

This is the post AIM6 version of Agda. Features include:

• Inductive families.
• The with-construct.
• Records.
• Termination checker for structural recursion.
• The Alonzo compiler.
• Fancily coloured Emacs mode.

Download

See the Version Policy for what the version number means.