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.