diff --git a/README.md b/README.md
index 95604a66a..1dc56a700 100644
--- a/README.md
+++ b/README.md
@@ -1,23 +1,69 @@
-# Kind-Core
+# Kind
 
-Kind is a minimal Proof Checker.
+Kind is a minimalist proof checker.
 
-Examples on [MonoBook](https://github.com/HigherOrderCO/MonoBook) (search for `.kind` files)
+Examples can be found in the [MonoBook](https://github.com/HigherOrderCO/MonoBook) (look for `.kind` files).
 
-# Usage
+## Usage
 
-1. Clone and install this project
+### Installation with Haskell and Cabal
 
-2. Use the `kind` command to check/run terms
+To install Kind using Haskell and Cabal, follow these steps:
 
-## Grammar:
+1. Clone the repository:
+   ```
+   git clone https://github.com/HigherOrderCO/Kind.git
+   ```
+
+2. Navigate to the project directory:
+   ```
+   cd Kind
+   ```
+
+3. Update Cabal's package list:
+   ```
+   cabal update
+   ```
+
+4. Build the project:
+   ```
+   cabal build
+   ```
+
+5. Install the Kind executable:
+   ```
+   cabal install
+   ```
+
+6. Verify the installation:
+   ```
+   kind --version
+   ```
+
+Note: Ensure that Haskell and Cabal are installed on your system and that Cabal's binary directory is in your PATH.
+
+### Usage
+
+Kind can be used with the following commands:
+
+- `kind check`: Checks all .kind files in the current directory and subdirectories
+- `kind check <name|path>`: Type-checks all definitions in the specified file
+- `kind run <name|path>`: Normalizes the specified definition
+- `kind show <name|path>`: Stringifies the specified definition
+- `kind to-js <name|path>`: Compiles the specified definition to JavaScript
+- `kind deps <name|path>`: Shows immediate dependencies of the specified definition
+- `kind rdeps <name|path>`: Shows all dependencies of the specified definition recursively
+- `kind help`: Shows the help message
+
+
+## Grammar
+
+The grammar of Kind is defined as follows:
 
 ```
-<Name> ::=
-  <alphanumeric-string>
+<Name> ::= <alphanumeric-string>
 
-<Numb> ::=
-  <json-number-literal>
+<Numb> ::= <json-number-literal>
 
 <Term> ::=
   | ALL: "∀(" <Name> ":" <Term> ")" <Term>
@@ -51,3 +97,17 @@ Examples on [MonoBook](https://github.com/HigherOrderCO/MonoBook) (search for `.
   | ">" | "==" | "!=" | "&"
   | "|" | "^"  | "<<" | ">>"
 ```
+
+This grammar defines the syntactic structure of the Kind language, including terms, constructors, operators, and other fundamental elements.
+
+
+### Prerequisites
+
+Before installing Kind, ensure that you have GHC (Glasgow Haskell Compiler) version 9.10.1 installed on your system. You can check your GHC version by running:
+
+```
+ghc --version
+```
+
+If you don't have GHC 9.10.1 installed, please visit the official Haskell website (https://www.haskell.org/ghc/) for installation instructions specific to your operating system.
+
diff --git a/example.md b/example.md
new file mode 100644
index 000000000..ab1f119ad
--- /dev/null
+++ b/example.md
@@ -0,0 +1,80 @@
+
+# main.kindc
+
+This file contains fundamental type and function definitions in Kind, a functional programming language with a dependent type system.
+
+## Basic Types
+
+### Bool
+
+Defines the boolean type with two constructors:
+
+```hs
+Bool : * = #[]{
+  #true{} : Bool
+  #false{} : Bool
+};
+```
+
+### Nat
+
+Defines the natural numbers type with two constructors:
+
+```hs
+Nat : * = #[]{
+  #zero{} : Nat
+  #succ{ pred: Nat } : Nat
+};
+```
+
+## Predicates and Equality
+
+### IsTrue
+
+A predicate that checks if a boolean is true:
+
+```hs
+IsTrue : ∀(b: Bool) * = λb #[b]{
+  #indeed{} : (IsTrue #true{})
+};
+```
+
+### Equal
+
+Defines propositional equality between two values of the same type:
+
+```hs
+Equal : ∀(T: *) ∀(a: T) ∀(b: T) * = λT λa λb #[a b]{
+  #refl{} : (Equal T a a)
+};
+```
+
+## Functions
+
+### rewrite
+
+A function that allows rewriting an equality proof:
+
+```hs
+rewrite
+: ∀(T: *)
+  ∀(a: T)
+  ∀(b: T)
+  ∀(e: (Equal T a b))
+  ∀(P: ∀(x: A) *)
+  ∀(x: (P a))
+  (P b)
+= λT λa λb λ{
+  #refl: λP λx x
+};
+```
+
+## Entry Point
+
+The program's entry point is defined as:
+
+```hs
+MAIN = rewrite;
+```
+
+This file serves as a foundation for fundamental definitions in Kind, including basic types, predicates, and equality manipulation functions.