-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Dependently typed elimination functions using singletons
--   
--   This library provides eliminators for inductive data types, leveraging
--   the power of the <tt>singletons</tt> library to allow dependently
--   typed elimination.
@package eliminators
@version 0.2


-- | Generate dependently typed elimination functions using Template
--   Haskell.
module Data.Eliminator.TH

-- | <tt><a>deriveElim</a> dataName</tt> generates a top-level elimination
--   function for the datatype <tt>dataName</tt>. The eliminator will
--   follow these naming conventions: The naming conventions are:
--   
--   <ul>
--   <li>If the datatype has an alphanumeric name, its eliminator will have
--   that name with <tt>elim</tt> prepended.</li>
--   <li>If the datatype has a symbolic name, its eliminator will have that
--   name with <tt>~&gt;</tt> prepended.</li>
--   </ul>
deriveElim :: Name -> Q [Dec]

-- | <tt><a>deriveElimNamed</a> funName dataName</tt> generates a top-level
--   elimination function named <tt>funName</tt> for the datatype
--   <tt>dataName</tt>.
deriveElimNamed :: String -> Name -> Q [Dec]


-- | Dependently typed elimination functions using <tt>singletons</tt>.
module Data.Eliminator
elimBool :: forall (p_api4 :: (~>) Bool Type) (s_api5 :: Bool). Sing s_api5 -> (@@) p_api4 False -> (@@) p_api4 True -> (@@) p_api4 s_api5
elimEither :: forall (a_ao1l :: Type) (b_ao1m :: Type) (p_apia :: (~>) (Either a_ao1l b_ao1m) Type) (s_apib :: Either a_ao1l b_ao1m). Sing s_apib -> (forall (f0_apic :: a_ao1l). Sing f0_apic -> (@@) p_apia (Left f0_apic)) -> (forall (f0_apid :: b_ao1m). Sing f0_apid -> (@@) p_apia (Right f0_apid)) -> (@@) p_apia s_apib
elimList :: forall (a_11 :: Type) (p_apGd :: (~>) ([] a_11) Type) (s_apGe :: [] a_11). Sing s_apGe -> (@@) p_apGd [] -> (forall (f0_apGf :: a_11). Sing f0_apGf -> forall (f1_apGg :: [a_11]). Sing f1_apGg -> (@@) p_apGd f1_apGg -> (@@) p_apGd ((:) f0_apGf f1_apGg)) -> (@@) p_apGd s_apGe
elimMaybe :: forall (a_11 :: Type) (p_apim :: (~>) (Maybe a_11) Type) (s_apin :: Maybe a_11). Sing s_apin -> (@@) p_apim Nothing -> (forall (f0_apio :: a_11). Sing f0_apio -> (@@) p_apim (Just f0_apio)) -> (@@) p_apim s_apin

-- | Although <a>Nat</a> is not actually an inductive data type in GHC, we
--   can pretend that it is using this eliminator.
elimNat :: forall (p :: Nat ~> Type) (n :: Nat). Sing n -> p @@ 0 -> (forall (k :: Nat). Sing k -> p @@ k -> p @@ (k + 1)) -> p @@ n
elimNonEmpty :: forall (a_ajh8 :: Type) (p_apiv :: (~>) (NonEmpty a_ajh8) Type) (s_apiw :: NonEmpty a_ajh8). Sing s_apiw -> (forall (f0_apix :: a_ajh8). Sing f0_apix -> forall (f1_apiy :: [a_ajh8]). Sing f1_apiy -> (@@) p_apiv ((:|) f0_apix f1_apiy)) -> (@@) p_apiv s_apiw
elimOrdering :: forall (p_apiE :: (~>) Ordering Type) (s_apiF :: Ordering). Sing s_apiF -> (@@) p_apiE LT -> (@@) p_apiE EQ -> (@@) p_apiE GT -> (@@) p_apiE s_apiF
elimTuple0 :: forall (p_apN7 :: (~>) () Type) (s_apN8 :: ()). Sing s_apN8 -> (@@) p_apN7 () -> (@@) p_apN7 s_apN8
elimTuple2 :: forall (a_11 :: Type) (b_12 :: Type) (p_apNa :: (~>) ((,) a_11 b_12) Type) (s_apNb :: (,) a_11 b_12). Sing s_apNb -> (forall (f0_apNc :: a_11). Sing f0_apNc -> forall (f1_apNd :: b_12). Sing f1_apNd -> (@@) p_apNa ((,) f0_apNc f1_apNd)) -> (@@) p_apNa s_apNb
elimTuple3 :: forall (a_11 :: Type) (b_12 :: Type) (c_13 :: Type) (p_apNj :: (~>) ((,,) a_11 b_12 c_13) Type) (s_apNk :: (,,) a_11 b_12 c_13). Sing s_apNk -> (forall (f0_apNl :: a_11). Sing f0_apNl -> forall (f1_apNm :: b_12). Sing f1_apNm -> forall (f2_apNn :: c_13). Sing f2_apNn -> (@@) p_apNj ((,,) f0_apNl f1_apNm f2_apNn)) -> (@@) p_apNj s_apNk
elimTuple4 :: forall (a_11 :: Type) (b_12 :: Type) (c_13 :: Type) (d_14 :: Type) (p_apNv :: (~>) ((,,,) a_11 b_12 c_13 d_14) Type) (s_apNw :: (,,,) a_11 b_12 c_13 d_14). Sing s_apNw -> (forall (f0_apNx :: a_11). Sing f0_apNx -> forall (f1_apNy :: b_12). Sing f1_apNy -> forall (f2_apNz :: c_13). Sing f2_apNz -> forall (f3_apNA :: d_14). Sing f3_apNA -> (@@) p_apNv ((,,,) f0_apNx f1_apNy f2_apNz f3_apNA)) -> (@@) p_apNv s_apNw
elimTuple5 :: forall (a_11 :: Type) (b_12 :: Type) (c_13 :: Type) (d_14 :: Type) (e_15 :: Type) (p_apNK :: (~>) ((,,,,) a_11 b_12 c_13 d_14 e_15) Type) (s_apNL :: (,,,,) a_11 b_12 c_13 d_14 e_15). Sing s_apNL -> (forall (f0_apNM :: a_11). Sing f0_apNM -> forall (f1_apNN :: b_12). Sing f1_apNN -> forall (f2_apNO :: c_13). Sing f2_apNO -> forall (f3_apNP :: d_14). Sing f3_apNP -> forall (f4_apNQ :: e_15). Sing f4_apNQ -> (@@) p_apNK ((,,,,) f0_apNM f1_apNN f2_apNO f3_apNP f4_apNQ)) -> (@@) p_apNK s_apNL
elimTuple6 :: forall (a_11 :: Type) (b_12 :: Type) (c_13 :: Type) (d_14 :: Type) (e_15 :: Type) (f_16 :: Type) (p_apO2 :: (~>) ((,,,,,) a_11 b_12 c_13 d_14 e_15 f_16) Type) (s_apO3 :: (,,,,,) a_11 b_12 c_13 d_14 e_15 f_16). Sing s_apO3 -> (forall (f0_apO4 :: a_11). Sing f0_apO4 -> forall (f1_apO5 :: b_12). Sing f1_apO5 -> forall (f2_apO6 :: c_13). Sing f2_apO6 -> forall (f3_apO7 :: d_14). Sing f3_apO7 -> forall (f4_apO8 :: e_15). Sing f4_apO8 -> forall (f5_apO9 :: f_16). Sing f5_apO9 -> (@@) p_apO2 ((,,,,,) f0_apO4 f1_apO5 f2_apO6 f3_apO7 f4_apO8 f5_apO9)) -> (@@) p_apO2 s_apO3
elimTuple7 :: forall (a_11 :: Type) (b_12 :: Type) (c_13 :: Type) (d_14 :: Type) (e_15 :: Type) (f_16 :: Type) (g_17 :: Type) (p_apOn :: (~>) ((,,,,,,) a_11 b_12 c_13 d_14 e_15 f_16 g_17) Type) (s_apOo :: (,,,,,,) a_11 b_12 c_13 d_14 e_15 f_16 g_17). Sing s_apOo -> (forall (f0_apOp :: a_11). Sing f0_apOp -> forall (f1_apOq :: b_12). Sing f1_apOq -> forall (f2_apOr :: c_13). Sing f2_apOr -> forall (f3_apOs :: d_14). Sing f3_apOs -> forall (f4_apOt :: e_15). Sing f4_apOt -> forall (f5_apOu :: f_16). Sing f5_apOu -> forall (f6_apOv :: g_17). Sing f6_apOv -> (@@) p_apOn ((,,,,,,) f0_apOp f1_apOq f2_apOr f3_apOs f4_apOt f5_apOu f6_apOv)) -> (@@) p_apOn s_apOo