Idris data types are declared using a similar syntax to Haskell data types. For example, natural numbers, an option type and lists are declared in the standard library:

data Nat = Z | S Nat data Maybe a = Nothing | Just a data List a = Nil | (::) a (List a)

Functions are implemented by pattern matching. For example, addition on natural numbers can be deﬁned as follows, again taken from the standard library:

(+) : Nat -> Nat -> Nat Z + y = y (S k) + y = S (k + y)

Like Haskell, functions such as `(+)`

above may be overloaded using *type classes*.

Vectors are lists which carry their size in the type. They are declared as follows in the standard library, using a syntax similar to that for Generalised Algebraic Data Types (GADTs) in Haskell:

infixr 5 :: data Vect : Nat -> Type -> Type where Nil : Vect Z a (::) : a -> Vect k a -> Vect (S k) a

We can deﬁne functions by pattern matching. The type of a function over `Vect`

will describe what happens to the lengths of the vectors involved. For example, `app`

appends two Vects, returning a vector which is the sum of the lengths of the inputs:

app : Vect n a -> Vect m a -> Vect (n + m) a app Nil ys = ys app (x :: xs) ys = x :: app xs ys

For more details, see the documentation.