From c00e729952fe9ae62ec8bf86e568c5b57041ea8e Mon Sep 17 00:00:00 2001
From: Victor Maia <victor.taelin@gmail.com>
Date: Sat, 23 Jul 2022 14:56:54 -0300
Subject: [PATCH] Expand README

---
 README.md | 88 +++++++++++++++++++++++--------------------------------
 1 file changed, 36 insertions(+), 52 deletions(-)

diff --git a/README.md b/README.md
index 40797225..5902a953 100644
--- a/README.md
+++ b/README.md
@@ -8,37 +8,20 @@ features a blazingly fast type-checker based on **optimal
 compile programs to [HVM](https://github.com/kindelia/hvm) and [Kindelia](https://github.com/kindelia/kindelia),
 and can be used to prove and verify mathematical theorems.
 
-Example
--------
+Examples
+--------
 
-Kind2 functions can be defined using an equational notation that is highly
-inspired by Haskell, Idris and Agda:
+Pure functions can be defined using an equational notation that resembles [Haskell](https://www.haskell.org/):
 
-```c
+```idris
 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:
+Mathematical theorems can be proved via inductive reasoning, as in [Idris](https://www.idris-lang.org/) and [Agda](https://wiki.portal.chalmers.se/agda/pmwiki.php):
 
-```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`
+```idris
 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 =
@@ -47,40 +30,41 @@ Nat.commutes (Succ a) b =
   (Equal.chain e0 e1)
 ```
 
+Normal programs can be written in a monadic syntax that is inspired by [Rust](https://www.rust-lang.org/) and [TypeScript](https://www.typescriptlang.org/):
+
+```idris
+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 ())
+}
+```
+
 For more examples, check the [Wikind](https://github.com/kindelia/wikind).
 
+Installation
+------------
+
+Install [Rust](https://www.rust-lang.org/tools/install) first, then enter:
+
+```
+cargo install kind2
+```
+
+Enter `kind2` on the terminal to make sure it worked.
+
 Usage
 -----
 
-1. Install:
-
-```
-cargo install --path .
-```
-
-2. Check a Kind2 file:
-
-```
-kind2 check example.kind2
-```
-
-3. Eval the Main term:
-
-```
-kind2 eval example.kind2
-```
-
-4. Compile to HVM:
-
-```
-kind2 to-hvm example.kind2
-```
-
-5. Compile to Kindelia:
-
-```
-kind2 to-kdl example.kind2
-```
+Command    | Usage                     | Note
+---------- | ------------------------- | --------------------------------------------------------------
+Check      | `kind2 check  file.kind2` | Checks all definitions.
+Eval       | `kind2 eval   file.kind2` | Runs using the type-checker's evaluator.
+Run        | `kind2 run    file.kind2` | Runs using HVM's evaluator, on Rust-mode.
+To-HVM     | `kind2 to-hvm file.kind2` | Generates a [.hvm](https://github.com/kindelia/hvm) file. Can then be compiled to C.
+To-KDL     | `kind2 to-kdl file.kind2` | Generates a [.kdl](https://github.com/kindelia/kindelia) file. Can then be deployed to Kindelia.
 
 Benchmarks
 ----------