one). The parameters provided in curly brackets may be omitted if they can be inferred. Dependently typed pattern matching In core type theory, induction and recursion principles are used to prove theorems about inductive types. In Agda, dependently typed pattern matching is used instead. For example, natural number addition can be defined like this: add zero n = n add (suc m) n = suc (add m n) This way of writing recursive functions/inductive proofs is more natural than applying raw induction principles. In Agda, dependently typed pattern matching is a primitive of the language; the core language lacks the induction/recursion principles that pattern matching translates to. Metavariables One of the distinctive features of Agda, when compared with other similar systems such as Coq, is heavy reliance on metavariables for program construction. For example, one can write functions like this in Agda: add : ℕ → ℕ → ℕ add x y = ? ? here is a metavariable. When interacting with the system in emacs mode, it will show the user expected type and allow them to refine the metavariable, i.e., to replace it with more detailed code. This feature allows incremental program construction in a way similar to tactics-based proof assistants such as Coq. Proof automation Programming in pure type theory involves a lot of tedious and repetitive proofs. Although Agda has no separate tactics language, it is possible to program useful tactics within Agda itself. Typically, this works by writing an Agda function that optionally returns a proof of some property of interest. A tactic is then constructed by running this function at type-checking time, for example using the following auxiliary definitions: data Maybe (A : Set) : Set where Just : A → Maybe A Nothing : Maybe A data isJust {A : Set} : Maybe A → Set where auto : ∀ {x} → isJust (Just x) Tactic : ∀ {A : Set} (x : Maybe A) → isJust x → A Tactic Nothing () Tactic (Just x) auto = x Given a function check-even : (n : ) → Maybe (Even n) that inputs a number and optionally returns a proof of its evenness, a tactic can then be constructed as follows: check-even-tactic : {n : ℕ} → isJust (check-even n) → Even n check-even-tactic {n} = Tactic (check-even n) lemma0 : Even zero lemma0 = check-even-tactic auto lemma2 : Even (suc (suc zero))