-- 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.3


-- | 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_aqHt :: (~>) Bool Type) (s_aqHu :: Bool). Sing s_aqHu -> (@@) p_aqHt False -> (@@) p_aqHt True -> (@@) p_aqHt s_aqHu
elimEither :: forall (a_apoK :: Type) (b_apoL :: Type) (p_aqHz :: (~>) (Either a_apoK b_apoL) Type) (s_aqHA :: Either a_apoK b_apoL). Sing s_aqHA -> (forall (f0_aqHB :: a_apoK). Sing f0_aqHB -> (@@) p_aqHz (Left f0_aqHB)) -> (forall (f0_aqHC :: b_apoL). Sing f0_aqHC -> (@@) p_aqHz (Right f0_aqHC)) -> (@@) p_aqHz s_aqHA
elimList :: forall (a_11 :: Type) (p_ar7Y :: (~>) ([] a_11) Type) (s_ar7Z :: [] a_11). Sing s_ar7Z -> (@@) p_ar7Y [] -> (forall (f0_ar80 :: a_11). Sing f0_ar80 -> forall (f1_ar81 :: [a_11]). Sing f1_ar81 -> (@@) p_ar7Y f1_ar81 -> (@@) p_ar7Y ((:) f0_ar80 f1_ar81)) -> (@@) p_ar7Y s_ar7Z
elimMaybe :: forall (a_11 :: Type) (p_aqHL :: (~>) (Maybe a_11) Type) (s_aqHM :: Maybe a_11). Sing s_aqHM -> (@@) p_aqHL Nothing -> (forall (f0_aqHN :: a_11). Sing f0_aqHN -> (@@) p_aqHL (Just f0_aqHN)) -> (@@) p_aqHL s_aqHM
elimNat :: forall (p_aqHU :: (~>) Nat Type) (s_aqHV :: Nat). Sing s_aqHV -> (@@) p_aqHU Z -> (forall (f0_aqHW :: Nat). Sing f0_aqHW -> (@@) p_aqHU f0_aqHW -> (@@) p_aqHU (S f0_aqHW)) -> (@@) p_aqHU s_aqHV
elimNonEmpty :: forall (a_akv1 :: Type) (p_aqI3 :: (~>) (NonEmpty a_akv1) Type) (s_aqI4 :: NonEmpty a_akv1). Sing s_aqI4 -> (forall (f0_aqI5 :: a_akv1). Sing f0_aqI5 -> forall (f1_aqI6 :: [a_akv1]). Sing f1_aqI6 -> (@@) p_aqI3 ((:|) f0_aqI5 f1_aqI6)) -> (@@) p_aqI3 s_aqI4
elimOrdering :: forall (p_aqIc :: (~>) Ordering Type) (s_aqId :: Ordering). Sing s_aqId -> (@@) p_aqIc LT -> (@@) p_aqIc EQ -> (@@) p_aqIc GT -> (@@) p_aqIc s_aqId
elimTuple0 :: forall (p_arfc :: (~>) () Type) (s_arfd :: ()). Sing s_arfd -> (@@) p_arfc () -> (@@) p_arfc s_arfd
elimTuple2 :: forall (a_11 :: Type) (b_12 :: Type) (p_arff :: (~>) ((,) a_11 b_12) Type) (s_arfg :: (,) a_11 b_12). Sing s_arfg -> (forall (f0_arfh :: a_11). Sing f0_arfh -> forall (f1_arfi :: b_12). Sing f1_arfi -> (@@) p_arff ((,) f0_arfh f1_arfi)) -> (@@) p_arff s_arfg
elimTuple3 :: forall (a_11 :: Type) (b_12 :: Type) (c_13 :: Type) (p_arfo :: (~>) ((,,) a_11 b_12 c_13) Type) (s_arfp :: (,,) a_11 b_12 c_13). Sing s_arfp -> (forall (f0_arfq :: a_11). Sing f0_arfq -> forall (f1_arfr :: b_12). Sing f1_arfr -> forall (f2_arfs :: c_13). Sing f2_arfs -> (@@) p_arfo ((,,) f0_arfq f1_arfr f2_arfs)) -> (@@) p_arfo s_arfp
elimTuple4 :: forall (a_11 :: Type) (b_12 :: Type) (c_13 :: Type) (d_14 :: Type) (p_arfA :: (~>) ((,,,) a_11 b_12 c_13 d_14) Type) (s_arfB :: (,,,) a_11 b_12 c_13 d_14). Sing s_arfB -> (forall (f0_arfC :: a_11). Sing f0_arfC -> forall (f1_arfD :: b_12). Sing f1_arfD -> forall (f2_arfE :: c_13). Sing f2_arfE -> forall (f3_arfF :: d_14). Sing f3_arfF -> (@@) p_arfA ((,,,) f0_arfC f1_arfD f2_arfE f3_arfF)) -> (@@) p_arfA s_arfB
elimTuple5 :: forall (a_11 :: Type) (b_12 :: Type) (c_13 :: Type) (d_14 :: Type) (e_15 :: Type) (p_arfP :: (~>) ((,,,,) a_11 b_12 c_13 d_14 e_15) Type) (s_arfQ :: (,,,,) a_11 b_12 c_13 d_14 e_15). Sing s_arfQ -> (forall (f0_arfR :: a_11). Sing f0_arfR -> forall (f1_arfS :: b_12). Sing f1_arfS -> forall (f2_arfT :: c_13). Sing f2_arfT -> forall (f3_arfU :: d_14). Sing f3_arfU -> forall (f4_arfV :: e_15). Sing f4_arfV -> (@@) p_arfP ((,,,,) f0_arfR f1_arfS f2_arfT f3_arfU f4_arfV)) -> (@@) p_arfP s_arfQ
elimTuple6 :: forall (a_11 :: Type) (b_12 :: Type) (c_13 :: Type) (d_14 :: Type) (e_15 :: Type) (f_16 :: Type) (p_arg7 :: (~>) ((,,,,,) a_11 b_12 c_13 d_14 e_15 f_16) Type) (s_arg8 :: (,,,,,) a_11 b_12 c_13 d_14 e_15 f_16). Sing s_arg8 -> (forall (f0_arg9 :: a_11). Sing f0_arg9 -> forall (f1_arga :: b_12). Sing f1_arga -> forall (f2_argb :: c_13). Sing f2_argb -> forall (f3_argc :: d_14). Sing f3_argc -> forall (f4_argd :: e_15). Sing f4_argd -> forall (f5_arge :: f_16). Sing f5_arge -> (@@) p_arg7 ((,,,,,) f0_arg9 f1_arga f2_argb f3_argc f4_argd f5_arge)) -> (@@) p_arg7 s_arg8
elimTuple7 :: forall (a_11 :: Type) (b_12 :: Type) (c_13 :: Type) (d_14 :: Type) (e_15 :: Type) (f_16 :: Type) (g_17 :: Type) (p_args :: (~>) ((,,,,,,) a_11 b_12 c_13 d_14 e_15 f_16 g_17) Type) (s_argt :: (,,,,,,) a_11 b_12 c_13 d_14 e_15 f_16 g_17). Sing s_argt -> (forall (f0_argu :: a_11). Sing f0_argu -> forall (f1_argv :: b_12). Sing f1_argv -> forall (f2_argw :: c_13). Sing f2_argw -> forall (f3_argx :: d_14). Sing f3_argx -> forall (f4_argy :: e_15). Sing f4_argy -> forall (f5_argz :: f_16). Sing f5_argz -> forall (f6_argA :: g_17). Sing f6_argA -> (@@) p_args ((,,,,,,) f0_argu f1_argv f2_argw f3_argx f4_argy f5_argz f6_argA)) -> (@@) p_args s_argt


-- | A crude imitation of an eliminator function for <a>Nat</a>.
module Data.Eliminator.TypeNats

-- | Although <a>Nat</a> is not actually an inductive data type in GHC, we
--   can (crudely) 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
