diff --git a/README.md b/README.md
index c201cf52..794c6e7a 100644
--- a/README.md
+++ b/README.md
@@ -1,7 +1,54 @@
 Kind2
 =====
 
-This repository is a WIP.
+Kind2 is a pure functional, lazy, non-garbage-collected, general-purpose,
+dependently typed programming language focusing on performance and usability. It
+features a blazingly fast type-checker that runs on the
+[HVM](https://github.com/kindelia/hvm) via
+[NbE](https://en.wikipedia.org/wiki/Normalisation_by_evaluation). It can also
+compile programs to HVM and [Kindelia](https://github.com/kindelia/kindelia),
+and can be prove and verify mathematical theorems.
+
+Example
+-------
+
+Kind2 functions can be defined using an equational notation that is highly
+inspired by Haskell, Idris and Agda:
+
+```c
+List.map <a: Type> <b: Type> (x: (List a)) (f: (x: a) b) : (List b)
+List.map a b (Nil t)       f = (Nil b)
+List.map a b (Cons t x xs) f = (Cons b (f x) (List.map xs f))
+```
+
+But they can also be defined in a conventional notation that is highly inspired
+by Rust and TypeScript:
+
+```c
+// Note: syntax on development
+// Prints the double of many numbers
+Main : (IO (Result () String)) {
+  ask limit = (IO.prompt "Enter limit:");
+  for x in (List.range limit) {
+    (IO.print "{} * 2 = {}" x (Nat.double x));
+  }
+  return (Ok ());
+}
+```
+
+Mathematical proofs are present as well:
+
+```c
+// For every number `a` and `b`, `a + b == b + a`
+Nat.commutes (a: Nat) (b: Nat) : (Nat.add a b) == (Nat.add b a)
+Nat.commutes Zero     b = (Nat.comm.a b)
+Nat.commutes (Succ a) b =
+  let e0 = (Equal.apply @x(Succ x) (Nat.commutes a b))
+  let e1 = (Equal.mirror (Nat.commutes.b b a))
+  (Equal.chain e0 e1)
+```
+
+For more examples, check [/example](/example).
 
 Usage
 -----
@@ -18,8 +65,31 @@ cargo install --path .
 kind2 check example.kind2
 ```
 
-3. Check a Kind2 file:
+3. Eval the Main term:
 
 ```
-kind2 run example.kind2
+kind2 eval example.kind2
 ```
+
+4. Compile to HVM:
+
+```
+kind2 to-hvm example.kind2
+```
+
+5. Compile to Kindelia:
+
+```
+kind2 to-kdl example.kind2
+```
+
+Benchmarks
+----------
+
+### Type-Checker
+
+TODO
+
+### Runtime
+
+TODO
diff --git a/example/example.kind2 b/example/example.kind2
index b5ee7f5f..c970ba2b 100644
--- a/example/example.kind2
+++ b/example/example.kind2
@@ -68,8 +68,8 @@ List.tail <a> (xs: (List a)) : (List a)
 List.tail a (Cons t x xs) = xs
 
 List.map <a> <b> (x: (List a)) (f: (x: a) b) : (List b)
-List.map a b (Nil t)       f = (Nil b)
-List.map a b (Cons t x xs) f = (Cons b (f x) (List.map a b xs f))
+List.map a b (Nil t)       f = Nil
+List.map a b (Cons t x xs) f = (Cons (f x) (List.map xs f))
 
 List.concat <a> (xs: (List a)) (ys: (List a)) : (List a)
 List.concat a (Cons u x xs) ys = (Cons u x (List.concat a xs ys))