diff --git a/Data/Type/Natural.hs b/Data/Type/Natural.hs
--- a/Data/Type/Natural.hs
+++ b/Data/Type/Natural.hs
@@ -8,6 +8,9 @@
                           -- * Natural Numbers
                           -- | Peano natural numbers. It will be promoted to the type-level natural number.
                           Nat(..),
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708
+                          SSym0, SSym1, ZSym0,
+#endif
                           -- | Singleton type for 'Nat'.
                           SNat, Sing (SZ, SS),
                           -- ** Smart constructors
@@ -16,10 +19,29 @@
                           sZ, sS,
                           -- ** Arithmetic functions and their singletons.
                           min, Min, sMin, max, Max, sMax,
-                          (:+:), (:+), (%+), (%:+), (:*:), (:*), (%:*), (%*),
-                          (:-:), (:-), (%:-), (%-),
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708
+                          MinSym0, MinSym1, MinSym2,
+                          MaxSym0, MaxSym1, MaxSym2,
+#endif
+                          (:+:), (:+),
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708
+                          (:+$), (:+$$), (:+$$$),
+#endif
+                          (%+), (%:+), (:*:),
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708
+                          (:*), (:*$), (:*$$), (:*$$$),
+#endif
+                          (%:*), (%*), (:-:), (:-),
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708
+                          (:-$), (:-$$), (:-$$$),
+#endif
+                          (%:-), (%-),
                           -- ** Type-level predicate & judgements
-                          Leq(..), (:<=), (:<<=), (%:<<=), LeqInstance,
+                          Leq(..), (:<=), (:<<=),
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708
+                          (:<<=$),(:<<=$$),(:<<=$$$), 
+#endif
+                          (%:<<=), LeqInstance,
                           boolToPropLeq, boolToClassLeq, propToClassLeq,
                           LeqTrueInstance, propToBoolLeq,
                           -- * Conversion functions
@@ -45,10 +67,20 @@
                           twelve, thirteen, fourteen, fifteen, sixteen, seventeen, eighteen, nineteen, twenty,
                           Zero, One, Two, Three, Four, Five, Six, Seven, Eight, Nine, Ten,
                           Eleven, Twelve, Thirteen, Fourteen, Fifteen, Sixteen, Seventeen, Eighteen, Nineteen, Twenty,
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708
+                          ZeroSym0, OneSym0, TwoSym0, ThreeSym0, FourSym0, FiveSym0, SixSym0,
+                          SevenSym0, EightSym0, NineSym0, TenSym0, ElevenSym0, TwelveSym0,
+                          ThirteenSym0, FourteenSym0, FifteenSym0, SixteenSym0, SeventeenSym0,
+                          EighteenSym0, NineteenSym0, TwentySym0,
+#endif
                           sZero, sOne, sTwo, sThree, sFour, sFive, sSix, sSeven, sEight, sNine, sTen, sEleven,
                           sTwelve, sThirteen, sFourteen, sFifteen, sSixteen, sSeventeen, sEighteen, sNineteen, sTwenty,
                           n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, n12, n13, n14, n15, n16, n17, n18, n19, n20,
                           N0, N1, N2, N3, N4, N5, N6, N7, N8, N9, N10, N11, N12, N13, N14, N15, N16, N17, N18, N19, N20,
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708
+
+                          N0Sym0, N1Sym0, N2Sym0, N3Sym0, N4Sym0, N5Sym0, N6Sym0, N7Sym0, N8Sym0, N9Sym0, N10Sym0, N11Sym0, N12Sym0, N13Sym0, N14Sym0, N15Sym0, N16Sym0, N17Sym0, N18Sym0, N19Sym0, N20Sym0,
+#endif
                           sN0, sN1, sN2, sN3, sN4, sN5, sN6, sN7, sN8, sN9, sN10, sN11, sN12, sN13, sN14,
                           sN15, sN16, sN17, sN18, sN19, sN20
                          ) where
@@ -67,49 +99,7 @@
 import Language.Haskell.TH.Quote
 import Unsafe.Coerce
 import Language.Haskell.TH
-
---------------------------------------------------
--- * Natural numbers and its singleton type
---------------------------------------------------
-singletons [d|
- data Nat = Z | S Nat
-            deriving (Show, Eq, Ord)
- |]
-
---------------------------------------------------
--- ** Arithmetic functions.
---------------------------------------------------
-
-singletons [d|
- -- | Minimum function.
- min :: Nat -> Nat -> Nat
- min Z     Z     = Z
- min Z     (S _) = Z
- min (S _) Z     = Z
- min (S m) (S n) = S (min m n)
-
- -- | Maximum function.
- max :: Nat -> Nat -> Nat
- max Z     Z     = Z
- max Z     (S n) = S n
- max (S n) Z     = S n
- max (S n) (S m) = S (max n m)
- |]
-
-singletons [d|
- (+) :: Nat -> Nat -> Nat
- Z   + n = n
- S m + n = S (m + n)
-
- (-) :: Nat -> Nat -> Nat
- n   - Z   = n
- S n - S m = n - m
- Z   - S _ = Z
-
- (*) :: Nat -> Nat -> Nat
- Z   * _ = Z
- S n * m = n * m + m
- |]
+import Data.Type.Natural.Definitions
 
 instance P.Num Nat where
   n - m = n - m
@@ -122,78 +112,9 @@
   fromInteger n | n P.< 0   = error "negative integer"
                 | otherwise = S $ P.fromInteger (n P.- 1)
 
-infixl 6 :-:, %:-, -
-
-type n :-: m = n :- m
-infixl 6 :+:, %+, %:+, :+
-
-type n :+: m = n :+ m
-
--- | Addition for singleton numbers.
-(%+) :: SNat n -> SNat m -> SNat (n :+: m)
-(%+) = (%:+)
-
-infixl 7 :*:, %*, %:*, :*
-
--- | Type-level multiplication.
-type n :*: m = n :* m
-
--- | Multiplication for singleton numbers.
-(%*) :: SNat n -> SNat m -> SNat (n :*: m)
-(%*) = (%:*)
-
 --------------------------------------------------
 -- ** Convenient synonyms
 --------------------------------------------------
-singletons [d|
- zero, one, two, three, four, five, six, seven, eight, nine, ten :: Nat           
- eleven, twelve, thirteen, fourteen, fifteen, sixteen, seventeen, eighteen, nineteen, twenty :: Nat           
- zero      = Z
- one       = S zero
- two       = S one
- three     = S two
- four      = S three
- five      = S four
- six       = S five
- seven     = S six
- eight     = S seven
- nine      = S eight
- ten       = S nine
- eleven    = S ten
- twelve    = S eleven
- thirteen  = S twelve
- fourteen  = S thirteen
- fifteen   = S fourteen
- sixteen   = S fifteen
- seventeen = S sixteen
- eighteen  = S seventeen
- nineteen  = S eighteen
- twenty    = S nineteen
- n0, n1, n2, n3, n4, n5, n6, n7, n8, n9 :: Nat
- n10, n11, n12, n13, n14, n15, n16, n17 :: Nat
- n18, n19, n20 :: Nat
- n0  = zero
- n1  = one
- n2  = two
- n3  = three
- n4  = four
- n5  = five
- n6  = six
- n7  = seven
- n8  = eight
- n9  = nine
- n10 = ten
- n11 = eleven
- n12 = twelve
- n13 = thirteen
- n14 = fourteen
- n15 = fifteen
- n16 = sixteen
- n17 = seventeen
- n18 = eighteen
- n19 = nineteen
- n20 = twenty
- |]
 
 #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708
 sZ :: SNat Z
@@ -213,14 +134,6 @@
 class (n :: Nat) :<= (m :: Nat)
 instance Z :<= n
 instance (n :<= m) => S n :<= S m
-
--- | Boolean-valued type-level comparison function.
-singletons [d|
- (<<=) :: Nat -> Nat -> Bool
- Z   <<= _   = True
- S _ <<= Z   = False
- S n <<= S m = n <<= m
- |]
 
 -- | Comparison via GADTs.
 data Leq (n :: Nat) (m :: Nat) where
diff --git a/Data/Type/Natural/Definitions.hs b/Data/Type/Natural/Definitions.hs
new file mode 100644
--- /dev/null
+++ b/Data/Type/Natural/Definitions.hs
@@ -0,0 +1,140 @@
+{-# LANGUAGE CPP, DataKinds, FlexibleContexts, FlexibleInstances, GADTs #-}
+{-# LANGUAGE KindSignatures, MultiParamTypeClasses, NoImplicitPrelude   #-}
+{-# LANGUAGE PolyKinds, RankNTypes, TemplateHaskell, TypeFamilies, ScopedTypeVariables       #-}
+{-# LANGUAGE TypeOperators, UndecidableInstances, StandaloneDeriving    #-}
+module Data.Type.Natural.Definitions where
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708
+import Data.Singletons.TH      (singletons)
+import Data.Singletons.Prelude hiding ((:<=), SOrd(..), MaxSym1, MaxSym0, MaxSym2
+                                      , MinSym1, MinSym0, MinSym2, Max, Min)
+#endif
+import           Data.Type.Monomorphic
+import           Prelude          (Int, Bool (..), Eq (..), Integral (..), Ord ((<)),
+                                   Show (..), error, id, otherwise, ($), (.), undefined)
+import qualified Prelude          as P
+import           Proof.Equational
+import Data.Constraint hiding ((:-))
+import Language.Haskell.TH.Quote
+import Unsafe.Coerce
+import Language.Haskell.TH
+
+--------------------------------------------------
+-- * Natural numbers and its singleton type
+--------------------------------------------------
+singletons [d|
+ data Nat = Z | S Nat
+            deriving (Show, Eq, Ord)
+ |]
+
+--------------------------------------------------
+-- ** Arithmetic functions.
+--------------------------------------------------
+
+singletons [d|
+ -- | Minimum function.
+ min :: Nat -> Nat -> Nat
+ min Z     Z     = Z
+ min Z     (S _) = Z
+ min (S _) Z     = Z
+ min (S m) (S n) = S (min m n)
+
+ -- | Maximum function.
+ max :: Nat -> Nat -> Nat
+ max Z     Z     = Z
+ max Z     (S n) = S n
+ max (S n) Z     = S n
+ max (S n) (S m) = S (max n m)
+ |]
+
+singletons [d|
+ (+) :: Nat -> Nat -> Nat
+ Z   + n = n
+ S m + n = S (m + n)
+
+ (-) :: Nat -> Nat -> Nat
+ n   - Z   = n
+ S n - S m = n - m
+ Z   - S _ = Z
+
+ (*) :: Nat -> Nat -> Nat
+ Z   * _ = Z
+ S n * m = n * m + m
+ |]
+
+infixl 6 :-:, %:-, -
+
+type n :-: m = n :- m
+infixl 6 :+:, %+, %:+, :+
+
+type n :+: m = n :+ m
+
+-- | Addition for singleton numbers.
+(%+) :: SNat n -> SNat m -> SNat (n :+: m)
+(%+) = (%:+)
+
+infixl 7 :*:, %*, %:*, :*
+
+-- | Type-level multiplication.
+type n :*: m = n :* m
+
+-- | Multiplication for singleton numbers.
+(%*) :: SNat n -> SNat m -> SNat (n :*: m)
+(%*) = (%:*)
+
+singletons [d|
+ zero, one, two, three, four, five, six, seven, eight, nine, ten :: Nat           
+ eleven, twelve, thirteen, fourteen, fifteen, sixteen, seventeen, eighteen, nineteen, twenty :: Nat           
+ zero      = Z
+ one       = S zero
+ two       = S one
+ three     = S two
+ four      = S three
+ five      = S four
+ six       = S five
+ seven     = S six
+ eight     = S seven
+ nine      = S eight
+ ten       = S nine
+ eleven    = S ten
+ twelve    = S eleven
+ thirteen  = S twelve
+ fourteen  = S thirteen
+ fifteen   = S fourteen
+ sixteen   = S fifteen
+ seventeen = S sixteen
+ eighteen  = S seventeen
+ nineteen  = S eighteen
+ twenty    = S nineteen
+ n0, n1, n2, n3, n4, n5, n6, n7, n8, n9 :: Nat
+ n10, n11, n12, n13, n14, n15, n16, n17 :: Nat
+ n18, n19, n20 :: Nat
+ n0  = zero
+ n1  = one
+ n2  = two
+ n3  = three
+ n4  = four
+ n5  = five
+ n6  = six
+ n7  = seven
+ n8  = eight
+ n9  = nine
+ n10 = ten
+ n11 = eleven
+ n12 = twelve
+ n13 = thirteen
+ n14 = fourteen
+ n15 = fifteen
+ n16 = sixteen
+ n17 = seventeen
+ n18 = eighteen
+ n19 = nineteen
+ n20 = twenty
+ |]
+
+-- | Boolean-valued type-level comparison function.
+singletons [d|
+ (<<=) :: Nat -> Nat -> Bool
+ Z   <<= _   = True
+ S _ <<= Z   = False
+ S n <<= S m = n <<= m
+ |]
diff --git a/type-natural.cabal b/type-natural.cabal
--- a/type-natural.cabal
+++ b/type-natural.cabal
@@ -2,7 +2,7 @@
 -- documentation, see http://haskell.org/cabal/users-guide/
 
 name:                type-natural
-version:             0.2.1.2
+version:             0.2.1.3
 synopsis:            Type-level natural and proofs of their properties.
 description:         Type-level natural numbers and proofs of their properties.
 homepage:            https://github.com/konn/type-natural
@@ -10,7 +10,7 @@
 license-file:        LICENSE
 author:              Hiromi ISHII
 maintainer:          konn.jinro_at_gmail.com
-copyright:           (C) Hiromi ISHII 2013
+copyright:           (C) Hiromi ISHII 2013-2014
 category:            Math
 build-type:          Simple
 cabal-version:       >=1.8
@@ -21,7 +21,7 @@
 
 library
   exposed-modules:     Data.Type.Natural, Data.Type.Ordinal
-  -- other-modules:       
+  other-modules:       Data.Type.Natural.Definitions
   build-depends:       base                     >= 4       && < 5
                ,       equational-reasoning     == 0.2.*
                ,       monomorphic              >= 0.0.3
@@ -30,4 +30,4 @@
   if impl(ghc < 7.8)
     build-depends:     singletons               == 0.8.*
   else
-    build-depends:     singletons               >= 0.10    && < 1.0
+    build-depends:     singletons               >= 1.0    && < 1.1