diff --git a/src/Data/Bool.hs b/src/Data/Bool.hs
index 70dc100..be6d432 100644
--- a/src/Data/Bool.hs
+++ b/src/Data/Bool.hs
@@ -10,6 +10,7 @@
 {-# LANGUAGE PolyKinds             #-}
 {-# LANGUAGE UnicodeSyntax         #-}
 
+-- | Defines the boolean type and logical operators
 module Data.Bool where
 
 import Data.TypeClass (Eq, Enum, Show)
@@ -25,7 +26,8 @@ singletons [d|
     F ∷ 𝔹 -- ^ False
     deriving (Eq, Show)
 
-  -- Logical operatos
+
+  -- * Logical operatos
 
   -- | Conjuction
   (∧) ∷ 𝔹 → 𝔹 → 𝔹
diff --git a/src/Data/Function.hs b/src/Data/Function.hs
index f685c31..c66b896 100644
--- a/src/Data/Function.hs
+++ b/src/Data/Function.hs
@@ -11,7 +11,7 @@
 {-# LANGUAGE PolyKinds             #-}
 {-# LANGUAGE UnicodeSyntax         #-}
 
-
+-- | Defines commonly used functions and combinators
 module Data.Function where
 
 -- | Identity Function
diff --git a/src/Data/Integer.hs b/src/Data/Integer.hs
index ca0cfb8..b08ceeb 100644
--- a/src/Data/Integer.hs
+++ b/src/Data/Integer.hs
@@ -1,3 +1,4 @@
+-- | An arbitrary-precision integers datatype
 module Data.Integer
   ( module GHC.Integer
   ) where
diff --git a/src/Data/Nat.hs b/src/Data/Nat.hs
index 4a58d76..b1b6991 100644
--- a/src/Data/Nat.hs
+++ b/src/Data/Nat.hs
@@ -11,6 +11,7 @@
 {-# LANGUAGE PolyKinds             #-}
 {-# LANGUAGE UnicodeSyntax         #-}
 
+-- | Defines natural numbers on both term and type level
 module Data.Nat where
 
 import Relation.Equality
@@ -86,13 +87,13 @@ instance Bounded ℕ where
   maxBound = (∞)
 
 
--- | Convert a natural into an "Integer"
+-- | Convert a natural into an 'Integer'
 toInteger ∷ ℕ → Integer
 toInteger Z     = 0
 toInteger (S n) = 1 T.+ toInteger n
 
 
--- | Convert na "Integer" into a natural
+-- | Convert an 'Integer' into a natural
 fromInteger ∷ Integer → ℕ
 fromInteger 0 = Z
 fromInteger n
diff --git a/src/Data/TypeClass.hs b/src/Data/TypeClass.hs
index 4c0d28d..5bb0ceb 100644
--- a/src/Data/TypeClass.hs
+++ b/src/Data/TypeClass.hs
@@ -1,3 +1,4 @@
+-- | Exports haskell built-in typeclasses
 module Data.TypeClass
   ( Eq(..)
   , Ord(..)
diff --git a/src/Data/Vec.hs b/src/Data/Vec.hs
index e68c96e..859e4ca 100644
--- a/src/Data/Vec.hs
+++ b/src/Data/Vec.hs
@@ -12,6 +12,9 @@
 {-# LANGUAGE PolyKinds             #-}
 {-# LANGUAGE UnicodeSyntax         #-}
 
+-- | Defines a vector type, analogous to a list, that achieves
+-- type-safe operation like resizing and concatenation by using
+-- new dependantly typed language features in haskell
 module Data.Vec where
 
 import Relation.Equality (gcastWith)
@@ -27,11 +30,13 @@ import qualified Data.TypeClass as T
 
 infixr 5 :-
 
+-- | The 'Vec' datatype
 data Vec (a ∷ ★) ∷ ℕ → ★ where
-  Nil  ∷ Vec a Z
-  (:-) ∷ a → Vec a n → Vec a (S n)
+  Nil  ∷ Vec a Z                   -- ^ empty 'Vec', length 0
+  (:-) ∷ a → Vec a n → Vec a (S n) -- ^ "cons" operator
 
 
+-- | 'String' type alias for vector of characters
 type String n = Vec Char n
 
 
@@ -49,11 +54,20 @@ instance SingI n ⇒ IsString (String n) where
   fromString = fromList
 
 
+
+-- * Conversions
+
+-- | Convert a 'Vec' into a List
 toList ∷ Vec a n → [a]
 toList Nil = []
 toList (x :- xs) = x : toList xs
 
 
+-- | Convert a List into a 'Vec'
+--
+-- It's not possible to convert an infinite list to a vector
+-- as haskell does not permit constructing infinite type,
+-- which the resulting vector length would be.
 fromList ∷ SingI n ⇒ [a] → Vec a n
 fromList = f sing
   where  f ∷ Sℕ n → [a] → Vec a n
@@ -61,84 +75,127 @@ fromList = f sing
          f (SS n) (x:xs) = x :- f n xs
 
 
+
+-- * Basic functions
+
+-- | Vector concatenation
 (⧺) ∷ Vec a n → Vec a m → Vec a (n :+ m)
 (⧺) (x :- xs) ys = x :- xs ⧺ ys
 (⧺) Nil       ys = ys
 
 
+-- | Given a nonempty 'Vec' returns the first element
+-- and the rest of the vector in a tuple.
+-- > uncons x ≡ (head x, tail x)
+uncons ∷ Vec a (S n) → (a, Vec a n)
+uncons (x :- xs) = (x, xs)
+
+
+-- | Returns the 'head' (ie the first element) of a nonempty 'Vec'.
 head ∷ Vec a (S n) → a
 head (x :- _) = x
 
 
+-- | Returns the last element of a nonempty 'Vec'.
 last ∷ Vec a (S n) → a
 last (x :- Nil)     = x
 last (x :- y :- ys) = last (y :- ys)
 
 
+-- | Applied to a nonempty 'Vec' returns everything but its first element.
+-- > x ≡ head x ⧺ tail x
 tail ∷ Vec a (S n) → Vec a n
 tail (_ :- xs) = xs
 
 
+-- | Applied to a nonempty 'Vec' returns everything but its last element.
+-- > x ≡ init x ⧺ last x
 init ∷ Vec a (S n) → Vec a n
 init (x :- Nil)     = Nil
 init (x :- y :- ys) = x :- init (y :- ys)
 
 
-uncons ∷ Vec a (S n) → (a, Vec a n)
-uncons (x :- xs) = (x, xs)
 
+-- * Length information
 
+-- | Test whether a 'Vec' has zero length.
 null ∷ Vec a n → 𝔹
 null Nil = T
 null _   = F
 
 
+-- | Returns the length (numbers of elements) of a 'Vec'.
 length ∷ Vec a n → ℕ
 length Nil       = Z
 length (_ :- xs) = S (length xs)
 
-
+-- | Same as 'length' but produces a singleton type 'Sℕ'.
 sLength ∷ Vec a n → Sℕ n
 sLength Nil       = SZ
 sLength (x :- xs) = SS (sLength xs)
 
 
+
+-- * Transforming and reducing a 'Vec'
+
+-- | Applies a function on every element of a 'Vec'.
 map ∷ (a → b) → Vec a n → Vec b n
 map _ Nil       = Nil
 map f (x :- xs) = f x :- map f xs
 
 
+-- | 'foldl' applied to a binary operator, a starting value
+-- and a 'Vec' reduces the vector to a single value obtained
+-- by sequentially applying the operation from the left to the right.
 foldl ∷ (a → b → a) → a → Vec b n → a
 foldl _ x Nil       = x
 foldl f x (y :- ys) = foldl f (f x y) ys
 
 
+-- | Same as "fold" but reduces the vector in the opposite
+-- direction: from the right to the left.
 foldr ∷ (a → b → b) → b → Vec a n → b
 foldr f x Nil     = x
 foldr f x (y:-ys) = f y (foldr f x ys)
 
 
+-- | Variant of 'foldl' which requires no starting value but
+-- applies only on nonempty 'Vec'
 foldl₁ ∷ (a → a → a) → Vec a (S n) → a
 foldl₁ f (x :- Nil)     = x
 foldl₁ f (x :- y :- ys) = foldl₁ f (f x y :- ys)
 
 
+-- | As for 'foldl', a variant of 'foldr' with no starting point
 foldr₁ ∷ (a → a → a) → Vec a (S n) → a
 foldr₁ f (x :- Nil)     = x
 foldr₁ f (x :- y :- ys) = f x (foldr₁ f (y :- ys))
 
 
+-- | Reverse the order of the element of a 'Vec'
+-- > reverse ∘ reverse = id
 reverse ∷ Vec a n → Vec a n
 reverse Nil       = Nil
 reverse (y :- ys) = gcastWith proof (reverse ys ⧺ (y :- Nil))
   where proof = succ_plus (sLength ys)
 
 
+-- | Applied to a singleton natural @n@ and a value produces
+-- a vector obtained by duplicating the value @n@ times
 replicate ∷ Sℕ n → a → Vec a n
 replicate SZ     _ = Nil
 replicate (SS n) a = a :- replicate n a
 
 
+-- | 'take' @n@ applied to a 'Vec', returns the first @n@ element
+-- of the vector
 take ∷ Sℕ n → Vec a m → Vec a n
 take SZ      _        = Nil
 take (SS n) (x :- xs) = x :- take n xs
+
+
+-- | 'drop' @n@ applied to a 'Vec', returns every element of
+-- the vector but the first @n@
+drop ∷ Sℕ n → Vec a m → Vec a (m :- n)
+drop SZ     x         = x
+drop (SS n) (x :- xs) = drop n xs
diff --git a/src/Relation/Equality.hs b/src/Relation/Equality.hs
index 19e4332..9d1d3ab 100644
--- a/src/Relation/Equality.hs
+++ b/src/Relation/Equality.hs
@@ -11,6 +11,8 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE UnicodeSyntax #-}
 
+-- | Defines equality relation on types and provides
+-- a simple interface to write proof on haskell types
 module Relation.Equality where
 
 import Data.Singletons (Sing)
@@ -44,4 +46,3 @@ castWith Refl x = x
 -- | Generalized form of cast
 gcastWith ∷ ∀ a b r. (a :≡ b) → ((a ~ b) ⇒ r) → r
 gcastWith Refl x = x
-