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.