## Agda Demo

May 2nd, 2008 by Nils Anders DanielssonToday I ran a hands-on Agda demonstration. The code written during the demo:

module LiveDemo where data ℕ : Set where zero : ℕ suc : ℕ -> ℕ _+_ : ℕ -> ℕ -> ℕ zero + n = n suc m + n = suc (m + n) infixr 5 _◅_ _++_ data Vec (a : Set) : ℕ -> Set where [] : Vec a zero _◅_ : {n : ℕ} -> a -> Vec a n -> Vec a (suc n) _++_ : forall {a m n} -> Vec a m -> Vec a n -> Vec a (m + n) [] ++ ys = ys (x ◅ xs) ++ ys = x ◅ xs ++ ys data Last {a : Set} : forall {n} -> Vec a n -> Set where [] : Last [] _▻_ : forall {n} (xs : Vec a n) (x : a) -> Last (xs ++ x ◅ []) last : forall {a n} (xs : Vec a n) -> Last xs last [] = [] last (x ◅ xs) with last xs last (x ◅ .[]) | [] = [] ▻ x last (x ◅ .(ys ++ y ◅ [])) | (ys ▻ y) = (x ◅ ys) ▻ y

Some exercises:

- Define an inductive family for natural numbers less than a given natural number.
- Use this family to define a safe lookup function for vectors.

If you want more exercises, check out the Agda courses from the Types Summer School 2007 and the LerNET Summer School 2008 (available from the Agda wiki). Conor’s Epigram lecture notes from the AFP Summer School 2004 also contain a bunch of exercises.