diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,14 @@
+# Changelog for [`clash-prelude` package](http://hackage.haskell.org/package/clash-prelude)
+
+## 0.4 *March 20th 2014*
+  * Add fixed-point integers
+  * Extend documentation
+  * 'bit' and 'testBit' functions give run-time errors on out-of-bound positions
+
+## 0.3 *March 14th 2014*
+  * Add Documentation
+  * Easy SNat literals for 0..1024, e.g. d4 = snat :: SNat 4
+  * Fix blockRamPow2
+
+## 0.2 *March 5th 2014*
+  * Initial release
diff --git a/clash-prelude.cabal b/clash-prelude.cabal
--- a/clash-prelude.cabal
+++ b/clash-prelude.cabal
@@ -1,8 +1,18 @@
 Name:                 clash-prelude
-Version:              0.3
+Version:              0.4
 Synopsis:             CAES Language for Synchronous Hardware - Prelude library
--- Description:
-Homepage:             http://clash.ewi.utwente.nl/
+Description:
+  CλaSH (pronounced ‘clash’) is a functional hardware description language that
+  borrows both its syntax and semantics from the functional programming language
+  Haskell. The merits of using a functional language to describe hardware comes
+  from the fact that combinational circuits can be directly modeled as
+  mathematical functions and that functional languages lend themselves very well
+  at describing and (de-)composing mathematical functions.
+  .
+  This package provides:
+  .
+  * Prelude library containing datatypes and functions for circuit design
+Homepage:             http://christiaanb.github.io/clash2/
 bug-reports:          http://github.com/christiaanb/clash-prelude/issues
 License:              BSD3
 License-file:         LICENSE
@@ -13,6 +23,7 @@
 Build-type:           Simple
 
 Extra-source-files:   README.md
+                      CHANGELOG.md
 
 Cabal-version:        >=1.10
 
@@ -28,6 +39,7 @@
 
   Exposed-modules:    CLaSH.Bit
                       CLaSH.Class.BitVector
+                      CLaSH.Class.Num
                       CLaSH.Prelude
                       CLaSH.Promoted.Bool
                       CLaSH.Promoted.Nat
@@ -35,6 +47,7 @@
                       CLaSH.Promoted.Nat.Literals
                       CLaSH.Promoted.Ord
                       CLaSH.Signal
+                      CLaSH.Sized.Fixed
                       CLaSH.Sized.Signed
                       CLaSH.Sized.Unsigned
                       CLaSH.Sized.Vector
diff --git a/src/CLaSH/Class/Num.hs b/src/CLaSH/Class/Num.hs
new file mode 100644
--- /dev/null
+++ b/src/CLaSH/Class/Num.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE MultiParamTypeClasses  #-}
+{-# LANGUAGE NoImplicitPrelude      #-}
+{-# LANGUAGE TypeFamilies           #-}
+module CLaSH.Class.Num where
+
+class Add a b where
+  type AResult a b
+  plus  :: a -> b -> AResult a b
+  minus :: a -> b -> AResult a b
+
+class Mult a b where
+  type MResult a b
+  mult :: a -> b -> MResult a b
diff --git a/src/CLaSH/Prelude.hs b/src/CLaSH/Prelude.hs
--- a/src/CLaSH/Prelude.hs
+++ b/src/CLaSH/Prelude.hs
@@ -7,17 +7,23 @@
 {-# OPTIONS_GHC -O0 -fno-omit-interface-pragmas #-}
 
 module CLaSH.Prelude
-  ( module Exported
-  , (<^>)
+  ( -- * Creating synchronous sequential circuits
+    (<^>)
   , registerP
+    -- * 'Arrow' interface for synchronous sequential circuits
   , Comp (..)
+  , (^^^)
   , registerC
   , simulateC
-  , (^^^)
+    -- * BlockRAM primitives
   , blockRam
   , blockRamPow2
+  , blockRamC
+  , blockRamPow2C
+    -- * Utility functions
   , window
   , windowD
+  , module Exported
   )
 where
 
@@ -27,11 +33,13 @@
 import Data.Bits                   as Exported
 import Data.Default                as Exported
 import CLaSH.Class.BitVector       as Exported
+import CLaSH.Class.Num             as Exported
 import CLaSH.Promoted.Bool         as Exported
 import CLaSH.Promoted.Nat          as Exported
 import CLaSH.Promoted.Nat.TH       as Exported
 import CLaSH.Promoted.Nat.Literals as Exported
 import CLaSH.Promoted.Ord          as Exported
+import CLaSH.Sized.Fixed           as Exported
 import CLaSH.Sized.Signed          as Exported
 import CLaSH.Sized.Unsigned        as Exported
 import CLaSH.Sized.Vector          as Exported
@@ -45,7 +53,7 @@
 -- > window4 :: Signal Int -> Vec 4 (Signal Int)
 -- > window4 = window
 -- >
--- > simulateP window4 [1,2,3,4,5,... = [<1,0,0,0>,<2,1,0,0>,<3,2,1,0>,<4,3,2,1>,<5,4,3,2>,...
+-- > simulateP window4 [1,2,3,4,5,... == [1:>0:>0:>0:>Nil, 2:>1:>0:>0:>Nil, 3:>2:>1:>0:>Nil, 4:>3:>2:>1:>Nil, 5:>4:>3:>2:>Nil,...
 window :: (KnownNat (n + 1), Default a)
        => Signal a
        -> Vec ((n + 1) + 1) (Signal a)
@@ -60,7 +68,7 @@
 -- > windowD3 :: Signal Int -> Vec 3 (Signal Int)
 -- > windowD3 = windowD
 -- >
--- > simulateP windowD3 [1,2,3,4,... = [<0,0,0>,<1,0,0>,<2,1,0>,<3,2,1>,<4,3,2>,...
+-- > simulateP windowD3 [1,2,3,4,... == [0:>0:>0:>Nil, 1:>0:>0:>Nil, 2:>1:>0:>Nil, 3:>2:>1:>Nil, 4:>3:>2:>Nil,...
 windowD :: (KnownNat (n + 1), Default a)
         => Signal a
         -> Vec (n + 1) (Signal a)
@@ -73,6 +81,9 @@
 -- | Create a synchronous function from a combinational function describing
 -- a mealy machine
 --
+-- > mac :: Int        -- Current state
+-- >     -> (Int,Int)  -- Input
+-- >     -> (Int,Int)  -- (Updated state, output)
 -- > mac s (x,y) = (s',s)
 -- >   where
 -- >     s' = x * y + s
@@ -80,11 +91,21 @@
 -- > topEntity :: (Signal Int, Signal Int) -> Signal Int
 -- > topEntity = mac <^> 0
 -- >
--- > simulateP topEntity [(1,1),(2,2),(3,3),(4,4),... = [0,1,5,14,30,...
+-- > simulateP topEntity [(1,1),(2,2),(3,3),(4,4),... == [0,1,5,14,30,...
+--
+-- Synchronous sequential functions can be composed just like their combinational counterpart:
+--
+-- > dualMac :: (Signal Int, Signal Int)
+-- >         -> (Signal Int, Signal Int)
+-- >         -> Signal Int
+-- > dualMac (a,b) (x,y) = s1 + s2
+-- >   where
+-- >     s1 = (mac <^> 0) (a,b)
+-- >     s2 = (mac <^> 0) (x,y)
 (<^>) :: (Pack i, Pack o)
-      => (s -> i -> (s,o)) -- ^ Transfer function in mealy machine form
-      -> s -- ^ Initial state
-      -> (SignalP i -> SignalP o) -- ^ Synchronous function with input and output matching that of the mealy machine
+      => (s -> i -> (s,o))        -- ^ Transfer function in mealy machine form: @state -> input -> (newstate,output)@
+      -> s                        -- ^ Initial state
+      -> (SignalP i -> SignalP o) -- ^ Synchronous sequential function with input and output matching that of the mealy machine
 f <^> iS = \i -> let (s',o) = unpack $ f <$> s <*> (pack i)
                      s      = register iS s'
                  in unpack o
@@ -95,7 +116,7 @@
 -- > rP :: (Signal Int,Signal Int) -> (Signal Int, Signal Int)
 -- > rP = registerP (8,8)
 -- >
--- > simulateP rP [(1,1),(2,2),(3,3),... = [(8,8),(1,1),(2,2),(3,3),...
+-- > simulateP rP [(1,1),(2,2),(3,3),... == [(8,8),(1,1),(2,2),(3,3),...
 registerP :: Pack a => a -> SignalP a -> SignalP a
 registerP i = unpack Prelude.. register i Prelude.. pack
 
@@ -105,12 +126,12 @@
 -- > bram40 :: Signal (Unsigned 6) -> Signal (Unsigned 6) -> Signal Bool -> Signal a -> Signal a
 -- > bram40 = blockRam d50
 blockRam :: forall n m a . (KnownNat n, KnownNat m, Pack a)
-         => SNat n -- ^ Size @n@ of the blockram
+         => SNat n              -- ^ Size @n@ of the blockram
          -> Signal (Unsigned m) -- ^ Write address @w@
          -> Signal (Unsigned m) -- ^ Read address @r@
-         -> Signal Bool -- ^ Write enable
-         -> Signal a -- ^ Value to write (at address @w@)
-         -> Signal a -- ^ Value of the 'blockRAM' at address @r@ from the previous clock cycle
+         -> Signal Bool         -- ^ Write enable
+         -> Signal a            -- ^ Value to write (at address @w@)
+         -> Signal a            -- ^ Value of the 'blockRAM' at address @r@ from the previous clock cycle
 blockRam n wr rd en din = pack $ (bram' <^> binit) (wr,rd,en,din)
   where
     binit :: (Vec n a,a)
@@ -124,21 +145,39 @@
              | otherwise = ram
         o'               = ram ! r
 
+-- | Create a blockRAM with space for @n@ elements
+--
+-- > bramC40 :: Comp (Unsigned 6, Unsigned 6, Bool, a) a
+-- > bramC40 = blockRamC d50
+blockRamC :: (KnownNat n, KnownNat m, Pack a)
+          => SNat n -- ^ Size @n@ of the blockram
+          -> Comp (Unsigned m, Unsigned m, Bool, a) a
+blockRamC n = C ((\(wr,rd,en,din) -> blockRam n wr rd en din) Prelude.. unpack)
+
 {-# INLINABLE blockRamPow2 #-}
 -- | Create a blockRAM with space for 2^@n@ elements
 --
 -- > bram32 :: Signal (Unsigned 5) -> Signal (Unsigned 5) -> Signal Bool -> Signal a -> Signal a
 -- > bram32 = blockRamPow2 d32
 blockRamPow2 :: (KnownNat n, KnownNat (2^n), Pack a)
-             => (SNat ((2^n) :: Nat))  -- ^ Size 2^@n@ of the blockram
+             => SNat ((2^n) :: Nat) -- ^ Size @2^n@ of the blockram
              -> Signal (Unsigned n) -- ^ Write address @w@
              -> Signal (Unsigned n) -- ^ Read address @r@
-             -> Signal Bool -- ^ Write enable
-             -> Signal a -- ^ Value to write (at address @w@)
-             -> Signal a -- ^ Value of the 'blockRAM' at address @r@ from the previous clock cycle
+             -> Signal Bool         -- ^ Write enable
+             -> Signal a            -- ^ Value to write (at address @w@)
+             -> Signal a            -- ^ Value of the 'blockRAM' at address @r@ from the previous clock cycle
 blockRamPow2 = blockRam
 
--- | 'Arrow' interface to synchronous functions
+-- | Create a blockRAM with space for 2^@n@ elements
+--
+-- > bramC32 :: Comp (Unsigned 5, Unsigned 5, Bool, a) a
+-- > bramC32 = blockRamPow2C d32
+blockRamPow2C :: (KnownNat n, KnownNat (2^n), Pack a)
+              => SNat ((2^n) :: Nat) -- ^ Size @2^n@ of the blockram
+              -> Comp (Unsigned n, Unsigned n, Bool, a) a
+blockRamPow2C n = C ((\(wr,rd,en,din) -> blockRamPow2 n wr rd en din) Prelude.. unpack)
+
+-- | 'Comp'onent: an 'Arrow' interface to synchronous sequential functions
 newtype Comp a b = C { asFunction :: Signal a -> Signal b }
 
 instance Category Comp where
@@ -164,13 +203,13 @@
 -- > rC :: Comp (Int,Int) (Int,Int)
 -- > rC = registerC (8,8)
 -- >
--- > simulateC rP [(1,1),(2,2),(3,3),... = [(8,8),(1,1),(2,2),(3,3),...
+-- > simulateC rP [(1,1),(2,2),(3,3),... == [(8,8),(1,1),(2,2),(3,3),...
 registerC :: a -> Comp a a
 registerC = C Prelude.. register
 
 -- | Simulate a 'Comp'onent given a list of samples
 --
--- > simulateC (registerC 8) [1, 2, 3, ... = [8, 1, 2, 3, ...
+-- > simulateC (registerC 8) [1, 2, 3, ... == [8, 1, 2, 3, ...
 simulateC :: Comp a b -> [a] -> [b]
 simulateC f = simulate (asFunction f)
 
@@ -178,6 +217,9 @@
 -- | Create a synchronous 'Comp'onent from a combinational function describing
 -- a mealy machine
 --
+-- > mac :: Int        -- Current state
+-- >     -> (Int,Int)  -- Input
+-- >     -> (Int,Int)  -- (Updated state, output)
 -- > mac s (x,y) = (s',s)
 -- >   where
 -- >     s' = x * y + s
@@ -185,8 +227,18 @@
 -- > topEntity :: Comp (Int,Int) Int
 -- > topEntity = mac ^^^ 0
 -- >
--- > simulateC topEntity [(1,1),(2,2),(3,3),(4,4),... = [0,1,5,14,30,...
-(^^^) :: (s -> i -> (s,o)) -> s -> Comp i o
+-- > simulateC topEntity [(1,1),(2,2),(3,3),(4,4),... == [0,1,5,14,30,...
+--
+-- Synchronous sequential must be composed using the 'Arrow' syntax
+--
+-- > dualMac :: Comp (Int,Int,Int,Int) Int
+-- > dualMac = proc (a,b,x,y) -> do
+-- >   rec s1 <- mac ^^^ 0 -< (a,b)
+-- >       s2 <- mac ^^^ 0 -< (x,y)
+-- >   returnA -< (s1 + s2)
+(^^^) :: (s -> i -> (s,o)) -- ^ Transfer function in mealy machine form: @state -> input -> (newstate,output)@
+      -> s                 -- ^ Initial state
+      -> Comp i o          -- ^ Synchronous sequential 'Comp'onent with input and output matching that of the mealy machine
 f ^^^ sI = C $ \i -> let (s',o) = unpack $ f <$> s <*> i
                          s      = register sI s'
                      in  o
diff --git a/src/CLaSH/Promoted/Nat.hs b/src/CLaSH/Promoted/Nat.hs
--- a/src/CLaSH/Promoted/Nat.hs
+++ b/src/CLaSH/Promoted/Nat.hs
@@ -4,7 +4,7 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeOperators       #-}
 module CLaSH.Promoted.Nat
-  ( SNat, snat, withSNat, fromSNat
+  ( SNat, snat, withSNat
   , UNat (..), toUNat, addUNat, multUNat, powUNat
   )
 where
@@ -29,11 +29,6 @@
   UZero :: UNat 0
   USucc :: UNat n -> UNat (n + 1)
 
--- | Convert a singleton natural number to an integer
-fromSNat :: SNat n -> Integer
-fromSNat (SNat p) = natVal p
-
-{-# NOINLINE fromSNat #-}
 -- | Convert a singleton natural number to it's unary representation
 toUNat :: SNat n -> UNat n
 toUNat (SNat p) = fromI (natVal p)
diff --git a/src/CLaSH/Signal.hs b/src/CLaSH/Signal.hs
--- a/src/CLaSH/Signal.hs
+++ b/src/CLaSH/Signal.hs
@@ -39,7 +39,7 @@
 -- Every element in the list will correspond to a value of the signal for one
 -- clock cycle.
 --
--- > sampleN 2 (fromList [1,2,3,4,5]) = [1,2]
+-- > sampleN 2 (fromList [1,2,3,4,5]) == [1,2]
 fromList :: [a] -> Signal a
 fromList []     = error "finite list"
 fromList (x:xs) = x :- fromList xs
@@ -58,7 +58,7 @@
 -- The elements in the list correspond to the values of the 'Signal' at
 -- consecutive clock cycles
 --
--- > sample s = [s0, s1, s2, s3, ...
+-- > sample s == [s0, s1, s2, s3, ...
 sample :: Signal a -> [a]
 sample ~(x :- xs) = x : sample xs
 
@@ -67,14 +67,14 @@
 -- The elements in the list correspond to the values of the 'Signal' at
 -- consecutive clock cycles
 --
--- > sampleN 3 s = [s0, s1, s2]
+-- > sampleN 3 s == [s0, s1, s2]
 sampleN :: Int -> Signal a -> [a]
 sampleN 0 _          = []
 sampleN n ~(x :- xs) = x : (sampleN (n-1) xs)
 
 -- | Create a constant 'Signal' from a combinational value
 --
--- > sample (signal 4) = [4, 4, 4, 4, ...
+-- > sample (signal 4) == [4, 4, 4, 4, ...
 signal :: a -> Signal a
 signal a = a :- signal a
 
@@ -107,13 +107,13 @@
 -- | 'register' @i s@ delays the values in 'Signal' @s@ for one cycle, and sets
 -- the value at time 0 to @i@
 --
--- > sampleN 3 (register 8 (fromList [1,2,3,4])) = [8,1,2]
+-- > sampleN 3 (register 8 (fromList [1,2,3,4])) == [8,1,2]
 register :: a -> Signal a -> Signal a
 register i s = i :- s
 
 -- | Simulate a ('Signal' -> 'Signal') function given a list of samples
 --
--- > simulate (register 8) [1, 2, 3, ... = [8, 1, 2, 3, ...
+-- > simulate (register 8) [1, 2, 3, ... == [8, 1, 2, 3, ...
 simulate :: (Signal a -> Signal b) -> [a] -> [b]
 simulate f = sample . f . fromList
 
@@ -134,7 +134,7 @@
 
 -- | Simulate a ('SignalP' -> 'SignalP') function given a list of samples
 --
--- > simulateP (unpack . register (8,8) . pack) [(1,1), (2,2), (3,3), ... = [(8,8), (1,1), (2,2), (3,3), ...
+-- > simulateP (unpack . register (8,8) . pack) [(1,1), (2,2), (3,3), ... == [(8,8), (1,1), (2,2), (3,3), ...
 simulateP :: (Pack a, Pack b) => (SignalP a -> SignalP b) -> [a] -> [b]
 simulateP f = simulate (pack . f . unpack)
 
@@ -263,7 +263,7 @@
 -- > add2 :: Signal Int -> Signal Int
 -- > add2 x = x <^(+)^> (signal 2)
 -- >
--- > simulate add2 [1,2,3, = [3,4,5,...
+-- > simulate add2 [1,2,3,... == [3,4,5,...
 (<^) :: Applicative f => f a -> (a -> b -> c) -> f b -> f c
 v <^ f = liftA2 f v
 
@@ -272,7 +272,7 @@
 -- > add2 :: Signal Int -> Signal Int
 -- > add2 x = x <^(+)^> (signal 2)
 -- >
--- > simulate add2 [1,2,3, = [3,4,5,...
+-- > simulate add2 [1,2,3,... == [3,4,5,...
 (^>) :: Applicative f => (f a -> f b) -> f a -> f b
 f ^> v = f v
 
diff --git a/src/CLaSH/Sized/Fixed.hs b/src/CLaSH/Sized/Fixed.hs
new file mode 100644
--- /dev/null
+++ b/src/CLaSH/Sized/Fixed.hs
@@ -0,0 +1,157 @@
+{-# LANGUAGE DataKinds            #-}
+{-# LANGUAGE FlexibleContexts     #-}
+{-# LANGUAGE KindSignatures       #-}
+{-# LANGUAGE ScopedTypeVariables  #-}
+{-# LANGUAGE TemplateHaskell      #-}
+{-# LANGUAGE TypeOperators        #-}
+{-# LANGUAGE TypeFamilies         #-}
+{-# LANGUAGE UndecidableInstances #-}
+module CLaSH.Sized.Fixed
+  ( -- * Signed fixed point
+    SFixed, sf, unSF
+    -- * Unsigned fixed point
+  , UFixed, uf, unUF
+  )
+where
+
+import Control.Arrow
+import Data.Bits
+import Data.Default
+import Data.Function
+import Data.List
+import Data.Maybe
+import Data.Proxy
+import Data.Ratio
+import GHC.TypeLits
+import Language.Haskell.TH
+import Language.Haskell.TH.Syntax(Lift(..))
+
+import CLaSH.Class.BitVector
+import CLaSH.Class.Num
+import CLaSH.Signal
+import CLaSH.Sized.Signed
+import CLaSH.Sized.Unsigned
+
+-- | Fixed point signed integer with @i@ integer bits and @f@ fractional bits
+--
+-- For now, overflow behaviour for the 'Num' functions is wrap-around, not saturate
+newtype SFixed (i :: Nat) (f :: Nat) = SF { unSF :: Signed   (i + f) }
+  deriving (Eq,Ord)
+
+-- | Fixed point unsigned integer with @i@ integer bits and @f@ fractional bits
+--
+-- For now, overflow behaviour for the 'Num' functions is wrap-around, not saturate
+newtype UFixed (i :: Nat) (f :: Nat) = UF { unUF :: Unsigned (i + f) }
+  deriving (Eq,Ord)
+
+fracShift :: KnownNat n => proxy n -> Int
+fracShift = fromInteger . natVal
+
+sf :: Signed (i + f) -> SFixed i f
+sf = SF
+
+uf :: Unsigned (i + f) -> UFixed i f
+uf = UF
+
+showFixed :: (Bits a, KnownNat n, Show a, Integral a) =>
+             (proxy n -> a) -> proxy n -> [Char]
+showFixed unRep f = show i ++ "." ++ (uncurry pad . second (show . numerator) .
+                                      fromJust . find ((==1) . denominator . snd) .
+                                      iterate (succ *** (*10)) . (,) 0 $ (nom % denom))
+    where
+      pad n str = replicate (n - length str) '0' ++ str
+      nF        = fracShift f
+      rep       = unRep f
+      i         = rep `shiftR` nF
+      nom       = toInteger rep .&. ((2 ^ nF) - 1)
+      denom     = 2 ^ nF
+
+instance (KnownNat (i + f), KnownNat f) => Show (SFixed i f) where
+  show = showFixed unSF
+
+instance (KnownNat (i + f), KnownNat f) => Show (UFixed i f) where
+  show = showFixed unUF
+
+multFixedS :: (KnownNat ((i + f) + (i + f)), KnownNat (i + f), KnownNat f)
+           => SFixed i f -> SFixed i f -> SFixed i f
+multFixedS (SF a) (SF b) = res
+  where
+    resM = mult a b
+    resS = resM `shiftR` (fracShift res)
+    res  = SF (resizeS resS)
+
+multFixedU :: (KnownNat ((i + f) + (i + f)), KnownNat (i + f), KnownNat f)
+           => UFixed i f -> UFixed i f -> UFixed i f
+multFixedU (UF a) (UF b) = res
+  where
+    resM = mult a b
+    resS = resM `shiftR` (fracShift res)
+    res  = UF (resizeU resS)
+
+fixedFromInteger :: (Bits a, KnownNat n, Num a)
+                 => (a -> proxy n) -> Integer -> proxy n
+fixedFromInteger toF i = res
+  where
+    res = toF (fromInteger i `shiftL` fracShift res)
+
+instance (KnownNat ((i + f) + (i + f)), KnownNat (i + f), KnownNat f) => Num (SFixed i f) where
+  (+)           = (SF .) . on (+) unSF
+  (*)           = multFixedS
+  (-)           = (SF .) . on (-) unSF
+  negate        = SF . negate . unSF
+  abs           = SF . abs . unSF
+  signum        = SF . signum . unSF
+  fromInteger   = fixedFromInteger SF
+
+instance (KnownNat ((i + f) + (i + f)), KnownNat (i + f), KnownNat f) => Num (UFixed i f) where
+  (+)           = (UF .) . on (+) unUF
+  (*)           = multFixedU
+  (-)           = (UF .) . on (-) unUF
+  negate        = UF . negate . unUF
+  abs           = UF . abs . unUF
+  signum        = UF . signum . unUF
+  fromInteger   = fixedFromInteger UF
+
+instance BitVector (SFixed i f) where
+  type BitSize (SFixed i f) = i + f
+  toBV   (SF s) = toBV s
+  fromBV bv     = SF (fromBV bv)
+
+instance BitVector (UFixed i f) where
+  type BitSize (UFixed i f) = i + f
+  toBV   (UF s) = toBV s
+  fromBV bv     = UF (fromBV bv)
+
+instance Pack (SFixed i f) where
+  type SignalP (SFixed i f) = Signal (SFixed i f)
+  pack   = id
+  unpack = id
+
+instance Pack (UFixed i f) where
+  type SignalP (UFixed i f) = Signal (UFixed i f)
+  pack   = id
+  unpack = id
+
+instance (KnownNat i, KnownNat f, KnownNat (i + f)) => Lift (SFixed i f) where
+  lift s@(SF i) = sigE [| SF i |] (decSFixed (natVal (asProxy s)) (natVal s))
+    where
+      asProxy :: SFixed n a -> Proxy n
+      asProxy _ = Proxy
+
+instance (KnownNat i, KnownNat f, KnownNat (i + f)) => Lift (UFixed i f) where
+  lift s@(UF i) = sigE [| UF i |] (decUFixed (natVal (asProxy s)) (natVal s))
+    where
+      asProxy :: UFixed n a -> Proxy n
+      asProxy _ = Proxy
+
+decSFixed :: Integer -> Integer -> TypeQ
+decSFixed i f = appT (appT (conT ''SFixed) (litT $ numTyLit i)) (litT $ numTyLit f)
+
+decUFixed :: Integer -> Integer -> TypeQ
+decUFixed i f = appT (appT (conT ''SFixed) (litT $ numTyLit i)) (litT $ numTyLit f)
+
+instance KnownNat (i + f) => Default (SFixed i f) where
+  def = SF 0
+
+instance KnownNat (i + f) => Default (UFixed i f) where
+  def = UF 0
diff --git a/src/CLaSH/Sized/Signed.hs b/src/CLaSH/Sized/Signed.hs
--- a/src/CLaSH/Sized/Signed.hs
+++ b/src/CLaSH/Sized/Signed.hs
@@ -1,10 +1,10 @@
-{-# LANGUAGE DataKinds           #-}
-{-# LANGUAGE FlexibleContexts    #-}
-{-# LANGUAGE KindSignatures      #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TemplateHaskell     #-}
-{-# LANGUAGE TypeFamilies        #-}
-{-# LANGUAGE TypeOperators       #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE KindSignatures        #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TemplateHaskell       #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeOperators         #-}
 
 {-# OPTIONS_GHC -fno-warn-missing-methods #-}
 
@@ -23,9 +23,11 @@
 
 import CLaSH.Bit
 import CLaSH.Class.BitVector
-import CLaSH.Promoted.Nat
+import CLaSH.Class.Num
+import CLaSH.Promoted.Ord
 import CLaSH.Sized.Vector
 
+-- | Arbitrary-width signed integer represented by @n@ bits
 newtype Signed (n :: Nat) = S Integer
 
 instance Eq (Signed n) where
@@ -61,11 +63,11 @@
   minBound = minBoundS
   maxBound = maxBoundS
 
-minBoundS,maxBoundS :: forall n . KnownNat n => Signed n
+minBoundS,maxBoundS :: KnownNat n => Signed n
 {-# NOINLINE minBoundS #-}
-minBoundS = S $ negate $ 2 ^ (fromSNat (snat :: SNat n) -1)
+minBoundS = let res = S $ negate $ 2 ^ (natVal res - 1) in res
 {-# NOINLINE maxBoundS #-}
-maxBoundS = S $ 2 ^ (fromSNat (snat :: SNat n) - 1) - 1
+maxBoundS = let res = S $ 2 ^ (natVal res - 1) - 1 in res
 
 instance KnownNat n => Num (Signed n) where
   (+)         = plusS
@@ -78,13 +80,13 @@
 
 plusS,minS,timesS :: KnownNat n => Signed n -> Signed n -> Signed n
 {-# NOINLINE plusS #-}
-plusS (S a) (S b) = fromIntegerS_inlineable $ a + b
+plusS (S a) (S b) = fromIntegerS_inlineable (a + b)
 
 {-# NOINLINE minS #-}
-minS (S a) (S b) = fromIntegerS_inlineable $ a - b
+minS (S a) (S b) = fromIntegerS_inlineable (a - b)
 
 {-# NOINLINE timesS #-}
-timesS (S a) (S b) = fromIntegerS_inlineable $ a * b
+timesS (S a) (S b) = fromIntegerS_inlineable (a * b)
 
 negateS,absS,signumS :: KnownNat n => Signed n -> Signed n
 {-# NOINLINE negateS #-}
@@ -96,7 +98,7 @@
 {-# NOINLINE signumS #-}
 signumS (S n) = fromIntegerS_inlineable (signum n)
 
-fromIntegerS,fromIntegerS_inlineable :: forall n . KnownNat n => Integer -> Signed (n :: Nat)
+fromIntegerS,fromIntegerS_inlineable :: KnownNat n => Integer -> Signed (n :: Nat)
 {-# NOINLINE fromIntegerS #-}
 fromIntegerS = fromIntegerS_inlineable
 {-# INLINABLE fromIntegerS_inlineable #-}
@@ -104,12 +106,32 @@
     | nS == 0   = S 0
     | otherwise = res
   where
-    nS  = fromSNat (snat :: SNat n)
+    nS  = natVal res
     sz  = 2 ^ (nS - 1)
     res = case divMod i sz of
             (s,i') | even s    -> S i'
                    | otherwise -> S (i' - sz)
 
+instance KnownNat (Max m n) => Add (Signed m) (Signed n) where
+  type AResult (Signed m) (Signed n) = Signed (Max m n)
+  plus  = plusS2
+  minus = minusS2
+
+plusS2, minusS2 :: KnownNat (Max m n) => Signed m -> Signed n -> Signed (Max m n)
+{-# NOINLINE plusS2 #-}
+plusS2 (S a) (S b) = fromIntegerS_inlineable (a + b)
+
+{-# NOINLINE minusS2 #-}
+minusS2 (S a) (S b) = fromIntegerS_inlineable (a - b)
+
+instance KnownNat (m + n) => Mult (Signed m) (Signed n) where
+  type MResult (Signed m) (Signed n) = Signed (m + n)
+  mult = multS2
+
+{-# NOINLINE multS2 #-}
+multS2 :: KnownNat (m + n) => Signed m -> Signed n -> Signed (m + n)
+multS2 (S a) (S b) = fromIntegerS_inlineable (a * b)
+
 instance KnownNat n => Real (Signed n) where
   toRational = toRational . toIntegerS
 
@@ -177,11 +199,29 @@
 
 {-# NOINLINE bitS #-}
 bitS :: KnownNat n => Int -> Signed n
-bitS = fromIntegerS_inlineable . bit
+bitS i = res
+  where
+    sz = finiteBitSizeS res
+    res | sz > i    = fromIntegerS_inlineable (bit i)
+        | otherwise = error $ concat [ "bit: "
+                                     , "Setting out-of-range bit position, size: "
+                                     , show sz
+                                     , ", position: "
+                                     , show i
+                                     ]
 
 {-# NOINLINE testBitS #-}
-testBitS :: Signed n -> Int -> Bool
-testBitS (S n) i = testBit n i
+testBitS :: KnownNat n => Signed n -> Int -> Bool
+testBitS s@(S n) i
+  | sz > i    = testBit n i
+  | otherwise = error $ concat [ "testBit: "
+                               , "Setting out-of-range bit position, size: "
+                               , show sz
+                               , ", position: "
+                               , show i
+                               ]
+  where
+    sz = finiteBitSizeS s
 
 shiftLS,shiftRS,rotateLS,rotateRS :: KnownNat n => Signed n -> Int -> Signed n
 {-# NOINLINE shiftLS #-}
@@ -207,8 +247,8 @@
   finiteBitSize = finiteBitSizeS
 
 {-# NOINLINE finiteBitSizeS #-}
-finiteBitSizeS :: forall n . KnownNat n => Signed n -> Int
-finiteBitSizeS _ = fromInteger $ fromSNat (snat :: SNat n)
+finiteBitSizeS :: KnownNat n => Signed n -> Int
+finiteBitSizeS i = let res = fromInteger (natVal i) in res
 
 instance Show (Signed n) where
   show (S n) = show n
@@ -217,7 +257,7 @@
   def = fromIntegerS 0
 
 instance KnownNat n => Lift (Signed n) where
-  lift (S i) = sigE [| fromIntegerS i |] (decSigned $ fromSNat (snat :: (SNat n)))
+  lift s@(S i) = sigE [| fromIntegerS i |] (decSigned (natVal s))
 
 decSigned :: Integer -> TypeQ
 decSigned n = appT (conT ''Signed) (litT $ numTyLit n)
@@ -249,15 +289,16 @@
 -- Increasing the size of the number replicates the sign bit to the left.
 -- Truncating a number to length L keeps the sign bit and the rightmost L-1 bits.
 --
-resizeS :: forall n m . (KnownNat n, KnownNat m) => Signed n -> Signed m
-resizeS s@(S n) | n' <= m'  = fromIntegerS_inlineable n
-                | otherwise = case l of
+resizeS :: (KnownNat n, KnownNat m) => Signed n -> Signed m
+resizeS s@(S n) | n' <= m'  = extend
+                | otherwise = trunc
+  where
+    n'     = fromInteger (natVal s)
+    m'     = fromInteger (natVal extend)
+    extend = fromIntegerS_inlineable n
+    trunc  = case toList (toBitVector s) of
                     (x:xs) -> fromBitList $ reverse $ x : (drop (n' - m') xs)
                     _      -> error "resizeS impossible case: empty list"
-  where
-    n' = fromInteger $ fromSNat (snat :: SNat n) :: Int
-    m' = fromInteger $ fromSNat (snat :: SNat m) :: Int
-    l  = toList $ toBitVector s
 
 {-# NOINLINE resizeS_wrap #-}
 -- | A resize operation that is sign-preserving on extension, but wraps on truncation.
diff --git a/src/CLaSH/Sized/Unsigned.hs b/src/CLaSH/Sized/Unsigned.hs
--- a/src/CLaSH/Sized/Unsigned.hs
+++ b/src/CLaSH/Sized/Unsigned.hs
@@ -1,10 +1,10 @@
-{-# LANGUAGE DataKinds           #-}
-{-# LANGUAGE FlexibleContexts    #-}
-{-# LANGUAGE KindSignatures      #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TemplateHaskell     #-}
-{-# LANGUAGE TypeFamilies        #-}
-{-# LANGUAGE TypeOperators       #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE KindSignatures        #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TemplateHaskell       #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeOperators         #-}
 
 {-# OPTIONS_GHC -fno-warn-missing-methods #-}
 
@@ -22,9 +22,11 @@
 
 import CLaSH.Bit
 import CLaSH.Class.BitVector
-import CLaSH.Promoted.Nat
+import CLaSH.Class.Num
+import CLaSH.Promoted.Ord
 import CLaSH.Sized.Vector
 
+-- | Arbitrary-width unsigned integer represented by @n@ bits
 newtype Unsigned (n :: Nat) = U Integer
 
 instance Eq (Unsigned n) where
@@ -61,8 +63,8 @@
   maxBound = maxBoundU
 
 {-# NOINLINE maxBoundU #-}
-maxBoundU :: forall n . KnownNat n => Unsigned n
-maxBoundU = U $ (2 ^ fromSNat (snat :: SNat n)) - 1
+maxBoundU :: KnownNat n => Unsigned n
+maxBoundU = let res = U ((2 ^ natVal res) - 1) in res
 
 instance KnownNat n => Num (Unsigned n) where
   (+)         = plusU
@@ -88,12 +90,32 @@
 signumU (U 0) = (U 0)
 signumU (U _) = (U 1)
 
-fromIntegerU,fromIntegerU_inlineable :: forall n . KnownNat n => Integer -> Unsigned (n :: Nat)
+fromIntegerU,fromIntegerU_inlineable :: KnownNat n => Integer -> Unsigned n
 {-# NOINLINE fromIntegerU #-}
 fromIntegerU = fromIntegerU_inlineable
 {-# INLINABLE fromIntegerU_inlineable #-}
-fromIntegerU_inlineable i = U $ i `mod` (2 ^ fromSNat (snat :: SNat n))
+fromIntegerU_inlineable i = let res = U (i `mod` (2 ^ natVal res)) in res
 
+instance KnownNat (Max m n) => Add (Unsigned m) (Unsigned n) where
+  type AResult (Unsigned m) (Unsigned n) = Unsigned (Max m n)
+  plus  = plusU2
+  minus = minusU2
+
+plusU2, minusU2 :: KnownNat (Max m n) => Unsigned m -> Unsigned n -> Unsigned (Max m n)
+{-# NOINLINE plusU2 #-}
+plusU2 (U a) (U b) = fromIntegerU_inlineable (a + b)
+
+{-# NOINLINE minusU2 #-}
+minusU2 (U a) (U b) = fromIntegerU_inlineable (a - b)
+
+instance KnownNat (m + n) => Mult (Unsigned m) (Unsigned n) where
+  type MResult (Unsigned m) (Unsigned n) = Unsigned (m + n)
+  mult = multU2
+
+{-# NOINLINE multU2 #-}
+multU2 :: KnownNat (m + n) => Unsigned m -> Unsigned n -> Unsigned (m + n)
+multU2 (U a) (U b) = fromIntegerU_inlineable (a * b)
+
 instance KnownNat n => Real (Unsigned n) where
   toRational = toRational . toIntegerU
 
@@ -156,11 +178,29 @@
 
 {-# NOINLINE bitU #-}
 bitU :: KnownNat n => Int -> Unsigned n
-bitU = fromIntegerU_inlineable . bit
+bitU i = res
+  where
+    sz = finiteBitSizeU res
+    res | sz > i    = fromIntegerU_inlineable (bit i)
+        | otherwise = error $ concat [ "bit: "
+                                     , "Setting out-of-range bit position, size: "
+                                     , show sz
+                                     , ", position: "
+                                     , show i
+                                     ]
 
 {-# NOINLINE testBitU #-}
-testBitU :: Unsigned n -> Int -> Bool
-testBitU (U n) i = testBit n i
+testBitU :: KnownNat n => Unsigned n -> Int -> Bool
+testBitU s@(U n) i
+  | sz > i    = testBit n i
+  | otherwise = error $ concat [ "testBit: "
+                               , "Setting out-of-range bit position, size: "
+                               , show sz
+                               , ", position: "
+                               , show i
+                               ]
+  where
+    sz = finiteBitSizeU s
 
 shiftLU,shiftRU,rotateLU,rotateRU :: KnownNat n => Unsigned n -> Int -> Unsigned n
 {-# NOINLINE shiftLU #-}
@@ -186,11 +226,11 @@
   finiteBitSize  = finiteBitSizeU
 
 {-# NOINLINE finiteBitSizeU #-}
-finiteBitSizeU :: forall n . KnownNat n => Unsigned n -> Int
-finiteBitSizeU _ = fromInteger $ fromSNat (snat :: SNat n)
+finiteBitSizeU :: KnownNat n => Unsigned n -> Int
+finiteBitSizeU u = fromInteger (natVal u)
 
-instance forall n . KnownNat n => Lift (Unsigned n) where
-  lift (U i) = sigE [| fromIntegerU i |] (decUnsigned $ fromSNat (snat :: (SNat n)))
+instance KnownNat n => Lift (Unsigned n) where
+  lift u@(U i) = sigE [| fromIntegerU i |] (decUnsigned (natVal u))
 
 decUnsigned :: Integer -> TypeQ
 decUnsigned n = appT (conT ''Unsigned) (litT $ numTyLit n)
diff --git a/src/CLaSH/Sized/Vector.hs b/src/CLaSH/Sized/Vector.hs
--- a/src/CLaSH/Sized/Vector.hs
+++ b/src/CLaSH/Sized/Vector.hs
@@ -1,5 +1,4 @@
 {-# LANGUAGE DataKinds           #-}
-{-# LANGUAGE ExplicitForAll      #-}
 {-# LANGUAGE FlexibleContexts    #-}
 {-# LANGUAGE GADTs               #-}
 {-# LANGUAGE KindSignatures      #-}
@@ -18,20 +17,21 @@
   , vreverse, vmap, vzipWith
   , vfoldr, vfoldl, vfoldr1, vfoldl1
   , vzip, vunzip
-  , (!), vreplace, maxIndex
+  , (!), vreplace, maxIndex, vlength
   , vtake, vtakeI, vdrop, vdropI, vexact, vselect, vselectI
   , vcopy, vcopyI, viterate, viterateI, vgenerate, vgenerateI
-  , toList, v
+  , toList, v, lazyV, asNatProxy
   )
 where
 
 import Control.Applicative
 import Data.Traversable
-import Data.Foldable hiding (toList)
+import Data.Foldable              hiding (toList)
+import Data.Proxy
 import GHC.TypeLits
-import Language.Haskell.TH (ExpQ)
+import Language.Haskell.TH        (ExpQ)
 import Language.Haskell.TH.Syntax (Lift(..))
-import Unsafe.Coerce (unsafeCoerce)
+import Unsafe.Coerce              (unsafeCoerce)
 
 import CLaSH.Promoted.Nat
 
@@ -68,22 +68,34 @@
 
 {-# NOINLINE vhead #-}
 -- | Extract the first element of a vector
+--
+-- > vhead (1:>2:>3:>Nil) == 1
+-- > vhead Nil            == TYPE ERROR
 vhead :: Vec (n + 1) a -> a
 vhead (x :> _) = x
 
 {-# NOINLINE vtail #-}
 -- | Extract the elements after the head of a vector
+--
+-- > vtail (1:>2:>3:>Nil) == (2:>3:>Nil)
+-- > vtail Nil            == TYPE ERROR
 vtail :: Vec (n + 1) a -> Vec n a
 vtail (_ :> xs) = unsafeCoerce xs
 
 {-# NOINLINE vlast #-}
 -- | Extract the last element of a vector
+--
+-- > vlast (1:>2:>3:>Nil) == 3
+-- > vlast Nil            == TYPE ERROR
 vlast :: Vec (n + 1) a -> a
 vlast (x :> Nil)     = x
 vlast (_ :> y :> ys) = vlast (y :> ys)
 
 {-# NOINLINE vinit #-}
 -- | Extract all the elements of a vector except the last element
+--
+-- > vinit (1:>2:>3:>Nil) == (1:>2:>Nil)
+-- > vinit Nil            == TYPE ERROR
 vinit :: Vec (n + 1) a -> Vec n a
 vinit (_ :> Nil)     = unsafeCoerce Nil
 vinit (x :> y :> ys) = unsafeCoerce (x :> vinit (y :> ys))
@@ -99,6 +111,9 @@
 {-# INLINEABLE (+>>) #-}
 -- | Add an element to the head of the vector, and extract all elements of the
 -- resulting vector except the last element
+--
+-- > 1 +>> (3:>4:>5:>Nil) == (1:>3:>4:>Nil)
+-- > 1 +>> Nil            == Nil
 (+>>) :: a -> Vec n a -> Vec n a
 s +>> xs = shiftIntoL s xs
 
@@ -111,6 +126,9 @@
 infixl 5 <:
 {-# INLINEABLE (<:) #-}
 -- | Add an element to the tail of the vector
+--
+-- > (3:>4:>5:>Nil) <: 1 == (3:>4:>5:>1:>Nil)
+-- > Nil            <: 1 == (1:>Nil)
 (<:) :: Vec n a -> a -> Vec (n + 1) a
 xs <: s = snoc s xs
 
@@ -125,6 +143,9 @@
 {-# INLINE (<<+) #-}
 -- | Add an element to the tail of the vector, and extract all elements of the
 -- resulting vector except the first element
+--
+-- > (3:>4:>5:>Nil) <<+ 1 == (4:>5:>1:>Nil)
+-- > Nil            <<+ 1 == Nil
 (<<+) :: Vec n a -> a -> Vec n a
 xs <<+ s = shiftIntoR s xs
 
@@ -137,11 +158,16 @@
 infixr 5 <++>
 {-# INLINE (<++>) #-}
 -- | Append two vectors
+--
+-- > (1:>2:>3:>Nil) <++> (7:>8:>Nil) = (1:>2:>3:>7:>8:>Nil)
 (<++>) :: Vec n a -> Vec m a -> Vec (n + m) a
 xs <++> ys = vappend xs ys
 
 {-# NOINLINE vsplit #-}
 -- | Split a vector into two vectors at the given point
+--
+-- > vsplit (snat :: SNat 3) (1:>2:>3:>7:>8:>Nil) == (1:>2:>3:>Nil, 7:>8:>Nil)
+-- > vsplit d3               (1:>2:>3:>7:>8:>Nil) == (1:>2:>3:>Nil, 7:>8:>Nil)
 vsplit :: SNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
 vsplit n xs = vsplitU (toUNat n) xs
 
@@ -158,6 +184,12 @@
 
 {-# NOINLINE vconcat #-}
 -- | Concatenate a vector of vectors
+--
+-- > vunconcat ((1:>2:>3:>Nil)    :>
+-- >            (4:>5:>6:>Nil)    :>
+-- >            (7:>8:>9:>Nil)    :>
+-- >            (10:>11:>12:>Nil) :>
+-- >            Nil)                  == (1:>2:>3:>4:>5:>6:>7:>8:>9:>10:>11:>12:>Nil)
 vconcat :: Vec n (Vec m a) -> Vec (n * m) a
 vconcat Nil       = Nil
 vconcat (x :> xs) = unsafeCoerce (vappend x (vconcat xs))
@@ -165,6 +197,11 @@
 {-# NOINLINE vunconcat #-}
 -- | Split a vector of (n * m) elements into a vector of vectors with length m,
 -- where m is given
+--
+-- > vunconcat d4 (1:>2:>3:>4:>5:>6:>7:>8:>9:>10:>11:>12:>Nil) == ((1:>2:>3:>4:>Nil)    :>
+-- >                                                               (5:>6:>7:>8:>Nil)    :>
+-- >                                                               (9:>10:>11:>12:>Nil) :>
+-- >                                                               Nil)
 vunconcat :: KnownNat n => SNat m -> Vec (n * m) a -> Vec n (Vec m a)
 vunconcat n xs = vunconcatU (withSNat toUNat) (toUNat n) xs
 
@@ -182,7 +219,7 @@
 {-# NOINLINE vmerge #-}
 -- | Merge two vectors, alternating their elements, i.e.,
 --
--- > vmerge <xn, ..., x2, x1>  <yn, ..., y2, y1> == <xn, yn, ..., x2, y2, x1, y1>
+-- > vmerge (xn :> ... :> x2 :> x1 :> Nil)  (yn :> ... :> y2 :> y1 :> Nil) == (xn :> yn :> ... :> x2 :> y2 :> x1 :> y1 :> Nil)
 --
 vmerge :: Vec n a -> Vec n a -> Vec (n + n) a
 vmerge Nil       Nil       = Nil
@@ -198,7 +235,7 @@
 -- | 'vmap' @f xs@ is the list obtained by applying @f@ to each element
 -- of @xs@, i.e.,
 --
--- > vmap f <xn, ..., x2, x1> == <f xn, ..., f x2, f x1>
+-- > vmap f (xn :> ... :> x2 :> x1 :> Nil) == (f xn :> ... :> f x2 :> f x1 :> Nil)
 vmap :: (a -> b) -> Vec n a -> Vec n b
 vmap _ Nil       = Nil
 vmap f (x :> xs) = f x :> vmap f xs
@@ -208,6 +245,8 @@
 -- as the first argument, instead of a tupling function.
 -- For example, @'vzipWith' (+)@ is applied to two vectors to produce the
 -- vector of corresponding sums.
+--
+-- > vzipWith f (xn :> ... :> x2 :> x1 :> Nil) (yn :> ... :> y2 :> y1 :> Nil) == (f xn yn :> ... :> f x2 y2 :> f x1 y1 :> Nil)
 vzipWith :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
 vzipWith _ Nil       Nil       = Nil
 vzipWith f (x :> xs) (y :> ys) = f x y :> (vzipWith f xs (unsafeCoerce ys))
@@ -217,7 +256,8 @@
 -- the right-identity of the operator), and a vector, reduces the vector
 -- using the binary operator, from right to left:
 --
--- > foldr f z <xn, ..., x2, x1> == xn `f` (... (x2 `f` (x1 `f` z))...)
+-- > vfoldr f z (xn :> ... :> x2 :> x1 :> Nil) == xn `f` (... (x2 `f` (x1 `f` z))...)
+-- > vfoldr r z Nil                            == z
 vfoldr :: (a -> b -> b) -> b -> Vec n a -> b
 vfoldr _ z Nil       = z
 vfoldr f z (x :> xs) = f x (vfoldr f z xs)
@@ -227,7 +267,8 @@
 -- the left-identity of the operator), and a vector, reduces the vector
 -- using the binary operator, from left to right:
 --
--- > vfoldl f z <xn, ..., x2, x1> == (...((z `f` xn)... `f` x2) `f` x1
+-- > vfoldl f z (xn :> ... :> x2 :> x1 :> Nil) == (...((z `f` xn)... `f` x2) `f` x1
+-- > vfoldl f z Nil                            == z
 vfoldl :: (b -> a -> b) -> b -> Vec n a -> b
 vfoldl _ z Nil       = z
 vfoldl f z (x :> xs) = vfoldl f (f z x) xs
@@ -235,6 +276,10 @@
 {-# NOINLINE vfoldr1 #-}
 -- | 'vfoldr1' is a variant of 'vfoldr' that has no starting value argument,
 -- and thus must be applied to non-empty vectors.
+--
+-- > vfoldr1 f (xn :> ... :> x3 :> x2 :> x1 :> Nil) == xn `f` (... (x3 `f` (x2 `f` x1))...)
+-- > vfoldr1 f (x1 :> Nil)                          == x1
+-- > vfoldr1 f Nil                                  == TYPE ERROR
 vfoldr1 :: (a -> a -> a) -> Vec (n + 1) a -> a
 vfoldr1 _ (x :> Nil)       = x
 vfoldr1 f (x :> (y :> ys)) = f x (vfoldr1 f (y :> ys))
@@ -242,11 +287,17 @@
 {-# INLINEABLE vfoldl1 #-}
 -- | 'vfoldl1' is a variant of 'vfoldl' that has no starting value argument,
 -- and thus must be applied to non-empty vectors.
+--
+-- > vfoldl f (xn :> xn1 :> ... :> x2 :> x1 :> Nil) == (...((xn `f` xn1)... `f` x2) `f` x1
+-- > vfoldl f (x1 :> Nil)                           == x1
+-- > vfoldl f Nil                                   == TYPE ERROR
 vfoldl1 :: (a -> a -> a) -> Vec (n + 1) a -> a
 vfoldl1 f xs = vfoldl f (vhead xs) (vtail xs)
 
 {-# NOINLINE vzip #-}
 -- | 'vzip' takes two lists and returns a list of corresponding pairs.
+--
+-- > vzip (xn :> ... :> x2 :> x1 :> Nil) (yn :> ... :> y2 :> y1 :> Nil) == ((xn,yn) :> ... :> ... (x2,y2) :> (x1,y1) :> Nil)
 vzip :: Vec n a -> Vec n b -> Vec n (a,b)
 vzip Nil       Nil       = Nil
 vzip (x :> xs) (y :> ys) = (x,y) :> (vzip xs (unsafeCoerce ys))
@@ -254,6 +305,8 @@
 {-# NOINLINE vunzip #-}
 -- | 'vunzip' transforms a list of pairs into a list of first components
 -- and a list of second components.
+--
+-- > vunzip ((xn,yn) :> ... :> ... (x2,y2) :> (x1,y1) :> Nil) == (xn :> ... :> x2 :> x1 :> Nil, yn :> ... :> y2 :> y1 :> Nil)
 vunzip :: Vec n (a,b) -> (Vec n a, Vec n b)
 vunzip Nil = (Nil,Nil)
 vunzip ((a,b) :> xs) = let (as,bs) = vunzip xs
@@ -275,17 +328,27 @@
 -- | Vector index (subscript) operator, descending from 'maxIndex', where the
 -- last element has subscript 0.
 --
--- > <1,2,3,4,5> ! 4 == 1
--- > <1,2,3,4,5> ! maxIndex == 1
--- > <1,2,3,4,5> ! 1 == 4
+-- > (1:>2:>3:>4:>5:>Nil) ! 4        == 1
+-- > (1:>2:>3:>4:>5:>Nil) ! maxIndex == 1
+-- > (1:>2:>3:>4:>5:>Nil) ! 1        == 4
+-- > (1:>2:>3:>4:>5:>Nil) ! 14       == RUNTIME ERROR: Out of bounds
 (!) :: (KnownNat n, Integral i) => Vec n a -> i -> a
 xs ! i = vindex_integer xs (toInteger i)
 
 {-# NOINLINE maxIndex #-}
--- | Index (subscript) of the head of the vector
-maxIndex :: forall n a . KnownNat n => Vec n a -> Integer
-maxIndex _ = fromSNat (snat :: SNat n) - 1
+-- | Index (subscript) of the head of the 'Vec'tor
+--
+-- > maxIndex (6 :> 7 :> 8 :> Nil) == 2
+maxIndex :: KnownNat n => Vec n a -> Integer
+maxIndex = subtract 1 . vlength
 
+{-# NOINLINE vlength #-}
+-- | Length of a 'Vec'tor as an Integer
+--
+-- > vlength (6 :> 7 :> 8 :> Nil) == 3
+vlength :: KnownNat n => Vec n a -> Integer
+vlength = natVal . asNatProxy
+
 {-# NOINLINE vreplaceM_integer #-}
 vreplaceM_integer :: Vec n a -> Integer -> a -> Maybe (Vec n a)
 vreplaceM_integer Nil       _ _ = Nothing
@@ -304,17 +367,19 @@
 -- | Replace an element of a vector at the given index (subscript), NB: vector
 -- elements have a descending subscript starting from 'maxIndex' and ending at 0
 --
--- > vreplace <1,2,3,4,5> 3 7 == <1,7,3,4,5>
+-- > vreplace (1:>2:>3:>4:>5:>Nil) 3 7 == (1:>7:>3:>4:>5:>Nil)
+-- > vreplace (1:>2:>3:>4:>5:>Nil) 0 7 == (1:>2:>3:>4:>7:>Nil)
+-- > vreplace (1:>2:>3:>4:>5:>Nil) 9 7 == RUNTIME ERROR: Out of bounds
 vreplace :: (KnownNat n, Integral i) => Vec n a -> i -> a -> Vec n a
 vreplace xs i y = vreplace_integer xs (toInteger i) y
 
 {-# NOINLINE vtake #-}
 -- | 'vtake' @n@, applied to a vector @xs@, returns the @n@-length prefix of @xs@
 --
--- > vtake (snat :: SNat 3) <1,2,3,4,5> == <1,2,3>
--- > vtake d3 <1,2,3,4,5> == <1,2,3>
--- > vtake (snat :: SNat 0) <1,2> == <>
--- > vtake (snat :: SNat 4) <1,2> == TYPE ERROR
+-- > vtake (snat :: SNat 3) (1:>2:>3:>4:>5:>Nil) == (1:>2:>3:>Nil)
+-- > vtake d3               (1:>2:>3:>4:>5:>Nil) == (1:>2:>3:>Nil)
+-- > vtake d0               (1:>2:>Nil)          == Nil
+-- > vtake d4               (1:>2:>Nil)          == TYPE ERROR
 vtake :: SNat m -> Vec (m + n) a -> Vec m a
 vtake n = fst . vsplit n
 
@@ -326,10 +391,10 @@
 {-# NOINLINE vdrop #-}
 -- | 'vdrop' @n xs@ returns the suffix of @xs@ after the first @n@ elements
 --
--- > vdrop (snat :: SNat 3) <1,2,3,4,5> == <4,5>
--- > vdrop d3 <1,2,3,4,5> == <4,5>
--- > vdrop (snat :: SNat 0) <1,2> == <1,2>
--- > vdrop (snat :: SNat 4) <1,2> == TYPE ERROR
+-- > vdrop (snat :: SNat 3) (1:>2:>3:>4:>5:>Nil) == (4:>5:>Nil)
+-- > vdrop d3               (1:>2:>3:>4:>5:>Nil) == (4:>5:>Nil)
+-- > vdrop d0               (1:>2:>Nil)          == (1:>2:>Nil)
+-- > vdrop d4               (1:>2:>Nil)          == TYPE ERROR
 vdrop :: SNat m -> Vec (m + n) a -> Vec n a
 vdrop n = snd . vsplit n
 
@@ -342,7 +407,8 @@
 -- | 'vexact' @n xs@ returns @n@'th element of @xs@, NB: vector elements
 -- have a descending subscript starting from 'maxIndex' and ending at 0
 --
--- > vexact (snat :: SNat 1) <1,2,3,4,5> == 4
+-- > vexact (snat :: SNat 1) (1:>2:>3:>4:>5:>Nil) == 4
+-- > vexact d1               (1:>2:>3:>4:>5:>Nil) == 4
 vexact :: SNat m -> Vec (m + (n + 1)) a -> a
 vexact n xs = vhead $ snd $ vsplit n (vreverse xs)
 
@@ -350,7 +416,8 @@
 -- | 'vselect' @f s n xs@ selects @n@ elements with stepsize @s@ and
 -- offset @f@ from @xs@
 --
--- vselect (snat :: SNat 1) (snat :: SNat 2) (snat :: SNat 3) <1,2,3,4,5,6,7,8> == <2,4,6>
+-- > vselect (snat :: SNat 1) (snat :: SNat 2) (snat :: SNat 3) (1:>2:>3:>4:>5:>6:>7:>8:>Nil) == (2:>4:>6:>Nil)
+-- > vselect d1 d2 d3                                           (1:>2:>3:>4:>5:>6:>7:>8:>Nil) == (2:>4:>6:>Nil)
 vselect :: ((f + (s * n) + 1) <= i)
         => SNat f
         -> SNat s
@@ -375,6 +442,9 @@
 
 {-# NOINLINE vcopy #-}
 -- | 'vcopy' @n a@ returns a vector that has @n@ copies of @a@
+--
+-- > vcopy (snat :: SNat 3) 6 == (6:>6:>6:>Nil)
+-- > vcopy d3 6               == (6:>6:>6:>Nil)
 vcopy :: SNat n -> a -> Vec n a
 vcopy n a = vreplicateU (toUNat n) a
 
@@ -383,7 +453,7 @@
 vreplicateU (USucc s) x = x :> vreplicateU s x
 
 {-# INLINEABLE vcopyI #-}
--- | 'vcopy' @a@ creates a vector with as many copies of @a@ as demanded by the
+-- | 'vcopyI' @a@ creates a vector with as many copies of @a@ as demanded by the
 -- context
 vcopyI :: KnownNat n => a -> Vec n a
 vcopyI = withSNat vcopy
@@ -392,7 +462,8 @@
 -- | 'viterate' @n f x@ returns a vector starting with @x@ followed by @n@
 -- repeated applications of @f@ to @x@
 --
--- > viterate (snat :: SNat 4) f x = <x, f x, f (f x), f (f (f x))>
+-- > viterate (snat :: SNat 4) f x == (x :> f x :> f (f x) :> f (f (f x)) :> Nil)
+-- > viterate d4 f x               == (x :> f x :> f (f x) :> f (f (f x)) :> Nil)
 viterate :: SNat n -> (a -> a) -> a -> Vec n a
 viterate n f a = viterateU (toUNat n) f a
 
@@ -410,7 +481,8 @@
 -- | 'vgenerate' @n f x@ returns a vector with @n@ repeated applications of @f@
 -- to @x@
 --
--- > vgenerate (snat :: SNat 4) f x = <f x, f (f x), f (f (f x)), f (f (f (f x)))>
+-- > vgenerate (snat :: SNat 4) f x == (f x :> f (f x) :> f (f (f x)) :> f (f (f (f x))) :> Nil)
+-- > vgenerate d4 f x               == (f x :> f (f x) :> f (f (f x)) :> f (f (f (f x))) :> Nil)
 vgenerate :: SNat n -> (a -> a) -> a -> Vec n a
 vgenerate n f a = viterate n f (f a)
 
@@ -427,7 +499,53 @@
 
 -- | Create a vector literal from a list literal
 --
--- > $(v [1::Signed 8,2,3,4,5]) == <1,2,3,4,5> :: Vec 5 (Signed 8)
+-- > $(v [1::Signed 8,2,3,4,5]) == (8:>2:>3:>4:>5:>Nil) :: Vec 5 (Signed 8)
 v :: Lift a => [a] -> ExpQ
 v []     = [| Nil |]
 v (x:xs) = [| x :> $(v xs) |]
+
+-- | 'Vec'tor as a 'Proxy' for 'Nat'
+asNatProxy :: Vec n a -> Proxy n
+asNatProxy _ = Proxy
+
+{-# NOINLINE lazyV #-}
+-- | For when your vector functions are too strict in their arguments
+--
+-- For example:
+--
+-- > -- Bubble sort for 1 iteration
+-- > sortV xs = vmap fst sorted <: (snd (vlast sorted))
+-- >  where
+-- >    lefts  = vhead xs :> vmap snd (vinit sorted)
+-- >    rights = vtail xs
+-- >    sorted = vzipWith compareSwapL lefts rights
+-- >
+-- > -- Compare and swap
+-- > compareSwapL a b = if a < b then (a,b)
+-- >                             else (b,a)
+--
+-- Will not terminate because 'vzipWith' is too strict in its left argument:
+--
+-- > *Main> sortV (4 :> 1 :> 2 :> 3 :> Nil)
+-- > <*** Exception: <<loop>>
+--
+-- In this case, adding 'lazyV' on 'vzipWith's left argument:
+--
+-- > sortVL xs = vmap fst sorted <: (snd (vlast sorted))
+-- >  where
+-- >    lefts  = vhead xs :> vmap snd (vinit sorted)
+-- >    rights = vtail xs
+-- >    sorted = vzipWith compareSwapL (lazyV lefts) rights
+--
+-- Results in a successful computation:
+--
+-- > *Main> sortVL (4 :> 1 :> 2 :> 3 :> Nil)
+-- > <1,2,3,4>
+lazyV :: KnownNat n
+      => Vec n a
+      -> Vec n a
+lazyV = lazyV' (vcopyI undefined)
+  where
+    lazyV' :: Vec n a -> Vec n a -> Vec n a
+    lazyV' Nil       _  = Nil
+    lazyV' (_ :> xs) ys = vhead ys :> lazyV' xs (vtail ys)