lemma2 = check-even-tactic auto The actual proof of each lemma will be automatically constructed at type-checking time. If the tactic fails, type-checking will fail. Additionally, to write more complex tactics, Agda has support for automation via reflection. The reflection mechanism allows one to quote program fragments into – or unquote them from – the abstract syntax tree. The way reflection is used is similar to the way Template Haskell works. Another mechanism for proof automation is proof search action in emacs mode. It enumerates possible proof terms (limited to 5 seconds), and if one of the terms fits the specification, it will be put in the meta variable where the action is invoked. This action accepts hints, e.g., which theorems and from which modules can be used, whether the action can use pattern matching, etc. Termination checking Agda is a total language, i.e., each program in it must terminate and all possible patterns must be matched. Without this feature, the logic behind the language becomes inconsistent, and it becomes possible to prove arbitrary statements. For termination checking, Agda uses the approach of the Foetus termination checker. Standard library Agda has an extensive de facto standard library, which includes many useful definitions and theorems about basic data structures, such as natural numbers, lists, and vectors. The library is in beta, and is under active development. Unicode One of the more notable features of Agda is a heavy reliance on Unicode in program source code. The standard emacs mode uses shortcuts for input, such as \Sigma for Σ. Backends There are two compiler backends, MAlonzo for Haskell and one for JavaScript. See also List of proof assistants References Further reading External links Introduction to Agda, a five-part YouTube playlist by Daniel Peebles Brutal Introduction to Dependent Types in Agda Agda Tutorial: "explore programming in Agda without theoretical background" Programming languages Dependently typed languages Functional languages Pattern matching programming languages Academic programming languages Statically typed programming languages Proof assistants Free software programmed in Haskell Haskell programming language family Cross-platform free software Free compilers and interpreters Chalmers University of Technology Programming languages created in 2007 2007 software