AgdaLight
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.
Features
- Datatypes.
- Definitions by pattern matching.
- Implicit arguments.
- First-order logic plugin.
- QuickCheck plugin.
- Inductive families.
- Signatures and structures (+signature subtyping).
- Command line interface.
- Pattern completeness checking.
- LaTeX compiler (great for writing papers).
Not in AgdaLight
- Termination checking.
- Fancy emacs interface.
- Module system.
Download
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