AgdaLight is a version of the Agda proof checker. It is much more volatile than Agda and it's main purpose is to serve as a test platform for cool new extensions that are too experimental to make it into the real system. Be warned that AgdaLight is an experimental system, features may disappear and the syntax may change without any notice.


Not in AgdaLight


AgdaLight is provided as is, with no guarantees what-so-ever. There is no documentation, but the distribution comes with a bunch of examples.

Download AgdaLight

Valid HTML 4.01! Disclaimer
Last modified: Wed 30 Aug 2006 05:51:36 PM CEST