content: {-# LANGUAGE CPP #-}
  {-# LANGUAGE DataKinds, TypeOperators, TypeFamilies #-}
  {-# LANGUAGE UndecidableInstances #-} -- see comment
  
  -- Needed to define (*) as a type family
  {-# LANGUAGE NoStarIsType #-}
  
  {-# OPTIONS_GHC -Wall #-}
  
  -- {-# OPTIONS_GHC -fno-warn-unused-imports #-} -- TEMP
  -- {-# OPTIONS_GHC -fno-warn-unused-binds   #-} -- TEMP
  
  -- | Simple type-level, Peano-style (unary) natural numbers
  
  module ConCat.Nat where
  
  -- TODO: exports
  
  data Nat = Z | S Nat
  
  -- So we don't need -fno-warn-unticked-promoted-constructors
  type Z = 'Z
  type S = 'S
  
  infixl 6 +
  
  -- | Sum of type-level numbers
  type family (a :: Nat) + (b :: Nat) :: Nat where
    a +  Z  = a
    a + S b = S (a + b)
  
  infixl 6 -
  
  -- Experiment:
  -- | Difference of type-level numbers
  type family a - b :: Nat where
    n   - Z   = n
    S n - S m = n - m
  
  infixl 7 *
  
  -- | Product of type-level numbers
  type family a * b :: Nat where
    a *  Z  = a
    a * S b = a + (a * b)
  
  --     Nested type family application
  --       in the type family application: a + (a * b)
  --     (Use UndecidableInstances to permit this)
  --     In the type instance declaration for ‘*’
  
  infixr 8 ^
  
  -- | Exponentiating type-level numbers
  type family a ^ b :: Nat where
    a ^   Z = S Z
    a ^ S b = a * (a ^ b)
  
  type N0  = Z
  
  -- Generated code
  -- 
  --   putStrLn $ unlines ["type N" ++ show (n+1) ++ " = S N" ++ show n | n <- [0..31]]
  
  type N1  = S N0
  type N2  = S N1
  type N3  = S N2
  type N4  = S N3
  type N5  = S N4
  type N6  = S N5
  type N7  = S N6
  type N8  = S N7
  type N9  = S N8
  type N10 = S N9
  type N11 = S N10
  type N12 = S N11
  type N13 = S N12
  type N14 = S N13
  type N15 = S N14
  type N16 = S N15
  type N17 = S N16
  type N18 = S N17
  type N19 = S N18
  type N20 = S N19
  type N21 = S N20
  type N22 = S N21
  type N23 = S N22
  type N24 = S N23
  type N25 = S N24
  type N26 = S N25
  type N27 = S N26
  type N28 = S N27
  type N29 = S N28
  type N30 = S N29
  type N31 = S N30
  type N32 = S N31
  