diff --git a/Data/Nat.hs b/Data/Nat.hs
--- a/Data/Nat.hs
+++ b/Data/Nat.hs
@@ -5,8 +5,8 @@
 
 module Data.Nat (
     Nat(..)
-  , (Data.Nat.+)
-  , (Data.Nat.*)
+  , natPlus
+  , natMul
   , SNat
   , Data.Singletons.Prelude.Sing(..)
   , (:*)
@@ -38,12 +38,25 @@
   Z * b = Z
   S a * b = b + (a * b) |])
 
+{-| This is the plain value-level version of addition on Nats. There's rarely a reason to use this;
+it's included for completeness. -}
+natPlus :: Nat -> Nat -> Nat
+natPlus = (Data.Nat.+)
+
+{-| Similarly to 'natPlus', this one is included for completeness. -}
+natMul :: Nat -> Nat -> Nat
+natMul = (Data.Nat.*)
+
+{-| Provides a shorthand for 'Nat'-s using "GHC.TypeLits", for example:
+
+>>> :kind! Lit 3
+Lit 3 :: Nat
+= 'S ('S ('S 'Z))
+-}
+
 type family Lit n where
   Lit 0 = Z
   Lit n = S (Lit (n Lit.- 1))
 
 type SLit n = Sing (Lit n)
-
-
-
 
diff --git a/singleton-nats.cabal b/singleton-nats.cabal
--- a/singleton-nats.cabal
+++ b/singleton-nats.cabal
@@ -1,6 +1,6 @@
 
 name:                singleton-nats
-version:             0.1.1.0
+version:             0.2.0.0
 synopsis:            Unary natural numbers relying on the singletons infrastructure.         
 license:             BSD3
 license-file:        LICENSE