Copyright	(C) 2016 Richard Eisenberg
License	BSD-style (see LICENSE)
Maintainer	Ryan Scott
Stability	experimental
Portability	non-portable
Safe Haskell	None
Language	GHC2021

Data.Function.Singletons

Contents

Prelude re-exports
Other combinators
Defunctionalization symbols

Description

Defines singleton versions of the definitions in Data.Function.

Because many of these definitions are produced by Template Haskell, it is not possible to create proper Haddock documentation. Please look up the corresponding operation in Data.Function. Also, please excuse the apparent repeated variable names. This is due to an interaction between Template Haskell and Haddock.

Synopsis

type family Id (a1 :: a) :: a where ...
sId :: forall a (t :: a). Sing t -> Sing (Apply (IdSym0 :: TyFun a a -> Type) t)
type family Const (a1 :: a) (a2 :: b) :: a where ...
sConst :: forall a b (t1 :: a) (t2 :: b). Sing t1 -> Sing t2 -> Sing (Apply (Apply (ConstSym0 :: TyFun a (b ~> a) -> Type) t1) t2)
type family ((a1 :: b ~> c) . (a2 :: a ~> b)) (a3 :: a) :: c where ...
(%.) :: forall b c a (t1 :: b ~> c) (t2 :: a ~> b) (t3 :: a). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply ((.@#@$) :: TyFun (b ~> c) ((a ~> b) ~> (a ~> c)) -> Type) t1) t2) t3)
type family Flip (a1 :: a ~> (b ~> c)) (a2 :: b) (a3 :: a) :: c where ...
sFlip :: forall a b c (t1 :: a ~> (b ~> c)) (t2 :: b) (t3 :: a). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply (FlipSym0 :: TyFun (a ~> (b ~> c)) (b ~> (a ~> c)) -> Type) t1) t2) t3)
type family (a1 :: a ~> b) $ (a2 :: a) :: b where ...
(%$) :: forall a b (t1 :: a ~> b) (t2 :: a). Sing t1 -> Sing t2 -> Sing (Apply (Apply (($@#@$) :: TyFun (a ~> b) (a ~> b) -> Type) t1) t2)
type family (a1 :: a) & (a2 :: a ~> b) :: b where ...
(%&) :: forall a b (t1 :: a) (t2 :: a ~> b). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((&@#@$) :: TyFun a ((a ~> b) ~> b) -> Type) t1) t2)
type family On (a1 :: b ~> (b ~> c)) (a2 :: a ~> b) (a3 :: a) (a4 :: a) :: c where ...
sOn :: forall b c a (t1 :: b ~> (b ~> c)) (t2 :: a ~> b) (t3 :: a) (t4 :: a). Sing t1 -> Sing t2 -> Sing t3 -> Sing t4 -> Sing (Apply (Apply (Apply (Apply (OnSym0 :: TyFun (b ~> (b ~> c)) ((a ~> b) ~> (a ~> (a ~> c))) -> Type) t1) t2) t3) t4)
data IdSym0 (a1 :: TyFun a a)
type family IdSym1 (a6989586621679180225 :: a) :: a where ...
data ConstSym0 (a1 :: TyFun a (b ~> a))
data ConstSym1 (a6989586621679180220 :: a) (b1 :: TyFun b a)
type family ConstSym2 (a6989586621679180220 :: a) (a6989586621679180221 :: b) :: a where ...
data (.@#@$) (a1 :: TyFun (b ~> c) ((a ~> b) ~> (a ~> c)))
data (a6989586621679180207 :: b ~> c) .@#@$$ (b1 :: TyFun (a ~> b) (a ~> c))
data ((a6989586621679180207 :: b ~> c) .@#@$$$ (a6989586621679180208 :: a ~> b)) (c1 :: TyFun a c)
type family ((a6989586621679180207 :: b ~> c) .@#@$$$$ (a6989586621679180208 :: a ~> b)) (a6989586621679180209 :: a) :: c where ...
data FlipSym0 (a1 :: TyFun (a ~> (b ~> c)) (b ~> (a ~> c)))
data FlipSym1 (a6989586621679180195 :: a ~> (b ~> c)) (b1 :: TyFun b (a ~> c))
data FlipSym2 (a6989586621679180195 :: a ~> (b ~> c)) (a6989586621679180196 :: b) (c1 :: TyFun a c)
type family FlipSym3 (a6989586621679180195 :: a ~> (b ~> c)) (a6989586621679180196 :: b) (a6989586621679180197 :: a) :: c where ...
data ($@#@$) (a1 :: TyFun (a ~> b) (a ~> b))
data (a6989586621679180176 :: a ~> b) $@#@$$ (b1 :: TyFun a b)
type family (a6989586621679180176 :: a ~> b) $@#@$$$ (a6989586621679180177 :: a) :: b where ...
data (&@#@$) (a1 :: TyFun a ((a ~> b) ~> b))
data (a6989586621679327005 :: a) &@#@$$ (b1 :: TyFun (a ~> b) b)
type family (a6989586621679327005 :: a) &@#@$$$ (a6989586621679327006 :: a ~> b) :: b where ...
data OnSym0 (a1 :: TyFun (b ~> (b ~> c)) ((a ~> b) ~> (a ~> (a ~> c))))
data OnSym1 (a6989586621679327018 :: b ~> (b ~> c)) (b1 :: TyFun (a ~> b) (a ~> (a ~> c)))
data OnSym2 (a6989586621679327018 :: b ~> (b ~> c)) (a6989586621679327019 :: a ~> b) (c1 :: TyFun a (a ~> c))
data OnSym3 (a6989586621679327018 :: b ~> (b ~> c)) (a6989586621679327019 :: a ~> b) (a6989586621679327020 :: a) (d :: TyFun a c)
type family OnSym4 (a6989586621679327018 :: b ~> (b ~> c)) (a6989586621679327019 :: a ~> b) (a6989586621679327020 :: a) (a6989586621679327021 :: a) :: c where ...

Prelude re-exports

type family Id (a1 :: a) :: a where ... Source #

Equations

Id (x :: a) = x

sId :: forall a (t :: a). Sing t -> Sing (Apply (IdSym0 :: TyFun a a -> Type) t) Source #

type family Const (a1 :: a) (a2 :: b) :: a where ... Source #

Equations

Const (x :: a) (_1 :: b) = x

sConst :: forall a b (t1 :: a) (t2 :: b). Sing t1 -> Sing t2 -> Sing (Apply (Apply (ConstSym0 :: TyFun a (b ~> a) -> Type) t1) t2) Source #

type family ((a1 :: b ~> c) . (a2 :: a ~> b)) (a3 :: a) :: c where ... infixr 9 Source #

Equations

((f :: k2 ~> k3) . (g :: k4 ~> k2)) (a_6989586621679180201 :: k4) = Apply (Apply (Apply (Apply (Lambda_6989586621679180213Sym0 :: TyFun (k2 ~> k3) (TyFun (k4 ~> k2) (TyFun k4 (TyFun k4 k3 -> Type) -> Type) -> Type) -> Type) f) g) a_6989586621679180201) a_6989586621679180201

(%.) :: forall b c a (t1 :: b ~> c) (t2 :: a ~> b) (t3 :: a). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply ((.@#@$) :: TyFun (b ~> c) ((a ~> b) ~> (a ~> c)) -> Type) t1) t2) t3) infixr 9 Source #

type family Flip (a1 :: a ~> (b ~> c)) (a2 :: b) (a3 :: a) :: c where ... Source #

Equations

Flip (f :: k2 ~> (k3 ~> k4)) (x :: k3) (y :: k2) = Apply (Apply f y) x

sFlip :: forall a b c (t1 :: a ~> (b ~> c)) (t2 :: b) (t3 :: a). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply (FlipSym0 :: TyFun (a ~> (b ~> c)) (b ~> (a ~> c)) -> Type) t1) t2) t3) Source #

type family (a1 :: a ~> b) $ (a2 :: a) :: b where ... infixr 0 Source #

Equations

(f :: k1 ~> k2) $ (x :: k1) = Apply f x

(%$) :: forall a b (t1 :: a ~> b) (t2 :: a). Sing t1 -> Sing t2 -> Sing (Apply (Apply (($@#@$) :: TyFun (a ~> b) (a ~> b) -> Type) t1) t2) infixr 0 Source #

Other combinators

type family (a1 :: a) & (a2 :: a ~> b) :: b where ... infixl 1 Source #

Equations

(x :: k1) & (f :: k1 ~> k2) = Apply f x

(%&) :: forall a b (t1 :: a) (t2 :: a ~> b). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((&@#@$) :: TyFun a ((a ~> b) ~> b) -> Type) t1) t2) infixl 1 Source #

type family On (a1 :: b ~> (b ~> c)) (a2 :: a ~> b) (a3 :: a) (a4 :: a) :: c where ... infixl 0 Source #

Equations

On (ty :: k2 ~> (k2 ~> k3)) (f :: k4 ~> k2) (a_6989586621679327009 :: k4) (a_6989586621679327011 :: k4) = Apply (Apply (Apply (Apply (Apply (Apply (Lambda_6989586621679327026Sym0 :: TyFun (k2 ~> (k2 ~> k3)) (TyFun (k4 ~> k2) (TyFun k4 (TyFun k4 (TyFun k4 (TyFun k4 k3 -> Type) -> Type) -> Type) -> Type) -> Type) -> Type) ty) f) a_6989586621679327009) a_6989586621679327011) a_6989586621679327009) a_6989586621679327011

sOn :: forall b c a (t1 :: b ~> (b ~> c)) (t2 :: a ~> b) (t3 :: a) (t4 :: a). Sing t1 -> Sing t2 -> Sing t3 -> Sing t4 -> Sing (Apply (Apply (Apply (Apply (OnSym0 :: TyFun (b ~> (b ~> c)) ((a ~> b) ~> (a ~> (a ~> c))) -> Type) t1) t2) t3) t4) infixl 0 Source #

Defunctionalization symbols

data IdSym0 (a1 :: TyFun a a) Source #

Instances

Instances details

SingI (IdSym0 :: TyFun a a -> Type) Source #
Instance details Defined in GHC.Base.Singletons Methods sing :: Sing (IdSym0 :: TyFun a a -> Type) #
SuppressUnusedWarnings (IdSym0 :: TyFun a a -> Type) Source #
Instance details Defined in GHC.Base.Singletons Methods suppressUnusedWarnings :: () #
type Apply (IdSym0 :: TyFun a a -> Type) (a6989586621679180225 :: a) Source #
Instance details Defined in GHC.Base.Singletons type Apply (IdSym0 :: TyFun a a -> Type) (a6989586621679180225 :: a) = Id a6989586621679180225

type family IdSym1 (a6989586621679180225 :: a) :: a where ... Source #

Equations

IdSym1 (a6989586621679180225 :: a) = Id a6989586621679180225

data ConstSym0 (a1 :: TyFun a (b ~> a)) Source #

Instances

Instances details

SingI (ConstSym0 :: TyFun a (b ~> a) -> Type) Source #
Instance details Defined in GHC.Base.Singletons Methods sing :: Sing (ConstSym0 :: TyFun a (b ~> a) -> Type) #
SuppressUnusedWarnings (ConstSym0 :: TyFun a (b ~> a) -> Type) Source #
Instance details Defined in GHC.Base.Singletons Methods suppressUnusedWarnings :: () #
type Apply (ConstSym0 :: TyFun a (b ~> a) -> Type) (a6989586621679180220 :: a) Source #
Instance details Defined in GHC.Base.Singletons type Apply (ConstSym0 :: TyFun a (b ~> a) -> Type) (a6989586621679180220 :: a) = ConstSym1 a6989586621679180220 :: TyFun b a -> Type

data ConstSym1 (a6989586621679180220 :: a) (b1 :: TyFun b a) Source #

Instances

Instances details

SingI1 (ConstSym1 :: a -> TyFun b a -> Type) Source #
Instance details Defined in GHC.Base.Singletons Methods liftSing :: forall (x :: a). Sing x -> Sing (ConstSym1 x :: TyFun b a -> Type) #
SingI d => SingI (ConstSym1 d :: TyFun b a -> Type) Source #
Instance details Defined in GHC.Base.Singletons Methods sing :: Sing (ConstSym1 d :: TyFun b a -> Type) #
SuppressUnusedWarnings (ConstSym1 a6989586621679180220 :: TyFun b a -> Type) Source #
Instance details Defined in GHC.Base.Singletons Methods suppressUnusedWarnings :: () #
type Apply (ConstSym1 a6989586621679180220 :: TyFun b a -> Type) (a6989586621679180221 :: b) Source #
Instance details Defined in GHC.Base.Singletons type Apply (ConstSym1 a6989586621679180220 :: TyFun b a -> Type) (a6989586621679180221 :: b) = Const a6989586621679180220 a6989586621679180221

type family ConstSym2 (a6989586621679180220 :: a) (a6989586621679180221 :: b) :: a where ... Source #

Equations

ConstSym2 (a6989586621679180220 :: a) (a6989586621679180221 :: b) = Const a6989586621679180220 a6989586621679180221

data (.@#@$) (a1 :: TyFun (b ~> c) ((a ~> b) ~> (a ~> c))) infixr 9 Source #

Instances

Instances details

SingI ((.@#@$) :: TyFun (b ~> c) ((a ~> b) ~> (a ~> c)) -> Type) Source #
Instance details Defined in GHC.Base.Singletons Methods sing :: Sing ((.@#@$) :: TyFun (b ~> c) ((a ~> b) ~> (a ~> c)) -> Type) #
SuppressUnusedWarnings ((.@#@$) :: TyFun (b ~> c) ((a ~> b) ~> (a ~> c)) -> Type) Source #
Instance details Defined in GHC.Base.Singletons Methods suppressUnusedWarnings :: () #
type Apply ((.@#@$) :: TyFun (b ~> c) ((a ~> b) ~> (a ~> c)) -> Type) (a6989586621679180207 :: b ~> c) Source #
Instance details Defined in GHC.Base.Singletons type Apply ((.@#@$) :: TyFun (b ~> c) ((a ~> b) ~> (a ~> c)) -> Type) (a6989586621679180207 :: b ~> c) = (.@#@$$) a6989586621679180207 :: TyFun (a ~> b) (a ~> c) -> Type

data (a6989586621679180207 :: b ~> c) .@#@$$ (b1 :: TyFun (a ~> b) (a ~> c)) infixr 9 Source #

Instances

Instances details

SingI1 ((.@#@$$) :: (b ~> c) -> TyFun (a ~> b) (a ~> c) -> Type) Source #
Instance details Defined in GHC.Base.Singletons Methods liftSing :: forall (x :: b ~> c). Sing x -> Sing ((.@#@$$) x :: TyFun (a ~> b) (a ~> c) -> Type) #
SingI d => SingI ((.@#@$$) d :: TyFun (a ~> b) (a ~> c) -> Type) Source #
Instance details Defined in GHC.Base.Singletons Methods sing :: Sing ((.@#@$$) d :: TyFun (a ~> b) (a ~> c) -> Type) #
SuppressUnusedWarnings ((.@#@$$) a6989586621679180207 :: TyFun (a ~> b) (a ~> c) -> Type) Source #
Instance details Defined in GHC.Base.Singletons Methods suppressUnusedWarnings :: () #
type Apply ((.@#@$$) a6989586621679180207 :: TyFun (a ~> b) (a ~> c) -> Type) (a6989586621679180208 :: a ~> b) Source #
Instance details Defined in GHC.Base.Singletons type Apply ((.@#@$$) a6989586621679180207 :: TyFun (a ~> b) (a ~> c) -> Type) (a6989586621679180208 :: a ~> b) = a6989586621679180207 .@#@$$$ a6989586621679180208

data ((a6989586621679180207 :: b ~> c) .@#@$$$ (a6989586621679180208 :: a ~> b)) (c1 :: TyFun a c) infixr 9 Source #

Instances

Instances details

SingI2 ((.@#@$$$) :: (b ~> c) -> (a ~> b) -> TyFun a c -> Type) Source #
Instance details Defined in GHC.Base.Singletons Methods liftSing2 :: forall (x :: b ~> c) (y :: a ~> b). Sing x -> Sing y -> Sing (x .@#@$$$ y) #
SingI d => SingI1 ((.@#@$$$) d :: (a ~> b) -> TyFun a c -> Type) Source #
Instance details Defined in GHC.Base.Singletons Methods liftSing :: forall (x :: a ~> b). Sing x -> Sing (d .@#@$$$ x) #
(SingI d1, SingI d2) => SingI (d1 .@#@$$$ d2 :: TyFun a c -> Type) Source #
Instance details Defined in GHC.Base.Singletons Methods sing :: Sing (d1 .@#@$$$ d2) #
SuppressUnusedWarnings (a6989586621679180207 .@#@$$$ a6989586621679180208 :: TyFun a c -> Type) Source #
Instance details Defined in GHC.Base.Singletons Methods suppressUnusedWarnings :: () #
type Apply (a6989586621679180207 .@#@$$$ a6989586621679180208 :: TyFun a c -> Type) (a6989586621679180209 :: a) Source #
Instance details Defined in GHC.Base.Singletons type Apply (a6989586621679180207 .@#@$$$ a6989586621679180208 :: TyFun a c -> Type) (a6989586621679180209 :: a) = (a6989586621679180207 . a6989586621679180208) a6989586621679180209

type family ((a6989586621679180207 :: b ~> c) .@#@$$$$ (a6989586621679180208 :: a ~> b)) (a6989586621679180209 :: a) :: c where ... infixr 9 Source #

Equations

((a6989586621679180207 :: b ~> c) .@#@$$$$ (a6989586621679180208 :: a ~> b)) (a6989586621679180209 :: a) = (a6989586621679180207 . a6989586621679180208) a6989586621679180209

data FlipSym0 (a1 :: TyFun (a ~> (b ~> c)) (b ~> (a ~> c))) Source #

Instances

Instances details

SingI (FlipSym0 :: TyFun (a ~> (b ~> c)) (b ~> (a ~> c)) -> Type) Source #
Instance details Defined in GHC.Base.Singletons Methods sing :: Sing (FlipSym0 :: TyFun (a ~> (b ~> c)) (b ~> (a ~> c)) -> Type) #
SuppressUnusedWarnings (FlipSym0 :: TyFun (a ~> (b ~> c)) (b ~> (a ~> c)) -> Type) Source #
Instance details Defined in GHC.Base.Singletons Methods suppressUnusedWarnings :: () #
type Apply (FlipSym0 :: TyFun (a ~> (b ~> c)) (b ~> (a ~> c)) -> Type) (a6989586621679180195 :: a ~> (b ~> c)) Source #
Instance details Defined in GHC.Base.Singletons type Apply (FlipSym0 :: TyFun (a ~> (b ~> c)) (b ~> (a ~> c)) -> Type) (a6989586621679180195 :: a ~> (b ~> c)) = FlipSym1 a6989586621679180195

data FlipSym1 (a6989586621679180195 :: a ~> (b ~> c)) (b1 :: TyFun b (a ~> c)) Source #

Instances

Instances details

SingI1 (FlipSym1 :: (a ~> (b ~> c)) -> TyFun b (a ~> c) -> Type) Source #
Instance details Defined in GHC.Base.Singletons Methods liftSing :: forall (x :: a ~> (b ~> c)). Sing x -> Sing (FlipSym1 x) #
SingI d => SingI (FlipSym1 d :: TyFun b (a ~> c) -> Type) Source #
Instance details Defined in GHC.Base.Singletons Methods sing :: Sing (FlipSym1 d) #
SuppressUnusedWarnings (FlipSym1 a6989586621679180195 :: TyFun b (a ~> c) -> Type) Source #
Instance details Defined in GHC.Base.Singletons Methods suppressUnusedWarnings :: () #
type Apply (FlipSym1 a6989586621679180195 :: TyFun b (a ~> c) -> Type) (a6989586621679180196 :: b) Source #
Instance details Defined in GHC.Base.Singletons type Apply (FlipSym1 a6989586621679180195 :: TyFun b (a ~> c) -> Type) (a6989586621679180196 :: b) = FlipSym2 a6989586621679180195 a6989586621679180196

data FlipSym2 (a6989586621679180195 :: a ~> (b ~> c)) (a6989586621679180196 :: b) (c1 :: TyFun a c) Source #

Instances

Instances details

SingI d => SingI1 (FlipSym2 d :: b -> TyFun a c -> Type) Source #
Instance details Defined in GHC.Base.Singletons Methods liftSing :: forall (x :: b). Sing x -> Sing (FlipSym2 d x) #
SingI2 (FlipSym2 :: (a ~> (b ~> c)) -> b -> TyFun a c -> Type) Source #
Instance details Defined in GHC.Base.Singletons Methods liftSing2 :: forall (x :: a ~> (b ~> c)) (y :: b). Sing x -> Sing y -> Sing (FlipSym2 x y) #
(SingI d1, SingI d2) => SingI (FlipSym2 d1 d2 :: TyFun a c -> Type) Source #
Instance details Defined in GHC.Base.Singletons Methods sing :: Sing (FlipSym2 d1 d2) #
SuppressUnusedWarnings (FlipSym2 a6989586621679180195 a6989586621679180196 :: TyFun a c -> Type) Source #
Instance details Defined in GHC.Base.Singletons Methods suppressUnusedWarnings :: () #
type Apply (FlipSym2 a6989586621679180195 a6989586621679180196 :: TyFun a c -> Type) (a6989586621679180197 :: a) Source #
Instance details Defined in GHC.Base.Singletons type Apply (FlipSym2 a6989586621679180195 a6989586621679180196 :: TyFun a c -> Type) (a6989586621679180197 :: a) = Flip a6989586621679180195 a6989586621679180196 a6989586621679180197

type family FlipSym3 (a6989586621679180195 :: a ~> (b ~> c)) (a6989586621679180196 :: b) (a6989586621679180197 :: a) :: c where ... Source #

Equations

FlipSym3 (a6989586621679180195 :: a ~> (b ~> c)) (a6989586621679180196 :: b) (a6989586621679180197 :: a) = Flip a6989586621679180195 a6989586621679180196 a6989586621679180197

data ($@#@$) (a1 :: TyFun (a ~> b) (a ~> b)) infixr 0 Source #

Instances

Instances details

SingI (($@#@$) :: TyFun (a ~> b) (a ~> b) -> Type) Source #
Instance details Defined in GHC.Base.Singletons Methods sing :: Sing (($@#@$) :: TyFun (a ~> b) (a ~> b) -> Type) #
SuppressUnusedWarnings (($@#@$) :: TyFun (a ~> b) (a ~> b) -> Type) Source #
Instance details Defined in GHC.Base.Singletons Methods suppressUnusedWarnings :: () #
type Apply (($@#@$) :: TyFun (a ~> b) (a ~> b) -> Type) (a6989586621679180176 :: a ~> b) Source #
Instance details Defined in GHC.Base.Singletons type Apply (($@#@$) :: TyFun (a ~> b) (a ~> b) -> Type) (a6989586621679180176 :: a ~> b) = ($@#@$$) a6989586621679180176

data (a6989586621679180176 :: a ~> b) $@#@$$ (b1 :: TyFun a b) infixr 0 Source #

Instances

Instances details

SingI1 (($@#@$$) :: (a ~> b) -> TyFun a b -> Type) Source #
Instance details Defined in GHC.Base.Singletons Methods liftSing :: forall (x :: a ~> b). Sing x -> Sing (($@#@$$) x) #
SingI d => SingI (($@#@$$) d :: TyFun a b -> Type) Source #
Instance details Defined in GHC.Base.Singletons Methods sing :: Sing (($@#@$$) d) #
SuppressUnusedWarnings (($@#@$$) a6989586621679180176 :: TyFun a b -> Type) Source #
Instance details Defined in GHC.Base.Singletons Methods suppressUnusedWarnings :: () #
type Apply (($@#@$$) a6989586621679180176 :: TyFun a b -> Type) (a6989586621679180177 :: a) Source #
Instance details Defined in GHC.Base.Singletons type Apply (($@#@$$) a6989586621679180176 :: TyFun a b -> Type) (a6989586621679180177 :: a) = a6989586621679180176 $ a6989586621679180177

type family (a6989586621679180176 :: a ~> b) $@#@$$$ (a6989586621679180177 :: a) :: b where ... infixr 0 Source #

Equations

(a6989586621679180176 :: a ~> b) $@#@$$$ (a6989586621679180177 :: a) = a6989586621679180176 $ a6989586621679180177

data (&@#@$) (a1 :: TyFun a ((a ~> b) ~> b)) infixl 1 Source #

Instances

Instances details

SingI ((&@#@$) :: TyFun a ((a ~> b) ~> b) -> Type) Source #
Instance details Defined in Data.Function.Singletons Methods sing :: Sing ((&@#@$) :: TyFun a ((a ~> b) ~> b) -> Type) #
SuppressUnusedWarnings ((&@#@$) :: TyFun a ((a ~> b) ~> b) -> Type) Source #
Instance details Defined in Data.Function.Singletons Methods suppressUnusedWarnings :: () #
type Apply ((&@#@$) :: TyFun a ((a ~> b) ~> b) -> Type) (a6989586621679327005 :: a) Source #
Instance details Defined in Data.Function.Singletons type Apply ((&@#@$) :: TyFun a ((a ~> b) ~> b) -> Type) (a6989586621679327005 :: a) = (&@#@$$) a6989586621679327005 :: TyFun (a ~> b) b -> Type

data (a6989586621679327005 :: a) &@#@$$ (b1 :: TyFun (a ~> b) b) infixl 1 Source #

Instances

Instances details

SingI1 ((&@#@$$) :: a -> TyFun (a ~> b) b -> Type) Source #
Instance details Defined in Data.Function.Singletons Methods liftSing :: forall (x :: a). Sing x -> Sing ((&@#@$$) x :: TyFun (a ~> b) b -> Type) #
SingI d => SingI ((&@#@$$) d :: TyFun (a ~> b) b -> Type) Source #
Instance details Defined in Data.Function.Singletons Methods sing :: Sing ((&@#@$$) d :: TyFun (a ~> b) b -> Type) #
SuppressUnusedWarnings ((&@#@$$) a6989586621679327005 :: TyFun (a ~> b) b -> Type) Source #
Instance details Defined in Data.Function.Singletons Methods suppressUnusedWarnings :: () #
type Apply ((&@#@$$) a6989586621679327005 :: TyFun (a ~> b) b -> Type) (a6989586621679327006 :: a ~> b) Source #
Instance details Defined in Data.Function.Singletons type Apply ((&@#@$$) a6989586621679327005 :: TyFun (a ~> b) b -> Type) (a6989586621679327006 :: a ~> b) = a6989586621679327005 & a6989586621679327006

type family (a6989586621679327005 :: a) &@#@$$$ (a6989586621679327006 :: a ~> b) :: b where ... infixl 1 Source #

Equations

(a6989586621679327005 :: a) &@#@$$$ (a6989586621679327006 :: a ~> b) = a6989586621679327005 & a6989586621679327006

data OnSym0 (a1 :: TyFun (b ~> (b ~> c)) ((a ~> b) ~> (a ~> (a ~> c)))) infixl 0 Source #

Instances

Instances details

SingI (OnSym0 :: TyFun (b ~> (b ~> c)) ((a ~> b) ~> (a ~> (a ~> c))) -> Type) Source #
Instance details Defined in Data.Function.Singletons Methods sing :: Sing (OnSym0 :: TyFun (b ~> (b ~> c)) ((a ~> b) ~> (a ~> (a ~> c))) -> Type) #
SuppressUnusedWarnings (OnSym0 :: TyFun (b ~> (b ~> c)) ((a ~> b) ~> (a ~> (a ~> c))) -> Type) Source #
Instance details Defined in Data.Function.Singletons Methods suppressUnusedWarnings :: () #
type Apply (OnSym0 :: TyFun (b ~> (b ~> c)) ((a ~> b) ~> (a ~> (a ~> c))) -> Type) (a6989586621679327018 :: b ~> (b ~> c)) Source #
Instance details Defined in Data.Function.Singletons type Apply (OnSym0 :: TyFun (b ~> (b ~> c)) ((a ~> b) ~> (a ~> (a ~> c))) -> Type) (a6989586621679327018 :: b ~> (b ~> c)) = OnSym1 a6989586621679327018 :: TyFun (a ~> b) (a ~> (a ~> c)) -> Type

data OnSym1 (a6989586621679327018 :: b ~> (b ~> c)) (b1 :: TyFun (a ~> b) (a ~> (a ~> c))) infixl 0 Source #

Instances

Instances details

SingI1 (OnSym1 :: (b ~> (b ~> c)) -> TyFun (a ~> b) (a ~> (a ~> c)) -> Type) Source #
Instance details Defined in Data.Function.Singletons Methods liftSing :: forall (x :: b ~> (b ~> c)). Sing x -> Sing (OnSym1 x :: TyFun (a ~> b) (a ~> (a ~> c)) -> Type) #
SingI d => SingI (OnSym1 d :: TyFun (a ~> b) (a ~> (a ~> c)) -> Type) Source #
Instance details Defined in Data.Function.Singletons Methods sing :: Sing (OnSym1 d :: TyFun (a ~> b) (a ~> (a ~> c)) -> Type) #
SuppressUnusedWarnings (OnSym1 a6989586621679327018 :: TyFun (a ~> b) (a ~> (a ~> c)) -> Type) Source #
Instance details Defined in Data.Function.Singletons Methods suppressUnusedWarnings :: () #
type Apply (OnSym1 a6989586621679327018 :: TyFun (a ~> b) (a ~> (a ~> c)) -> Type) (a6989586621679327019 :: a ~> b) Source #
Instance details Defined in Data.Function.Singletons type Apply (OnSym1 a6989586621679327018 :: TyFun (a ~> b) (a ~> (a ~> c)) -> Type) (a6989586621679327019 :: a ~> b) = OnSym2 a6989586621679327018 a6989586621679327019

data OnSym2 (a6989586621679327018 :: b ~> (b ~> c)) (a6989586621679327019 :: a ~> b) (c1 :: TyFun a (a ~> c)) infixl 0 Source #

Instances

Instances details

SingI2 (OnSym2 :: (b ~> (b ~> c)) -> (a ~> b) -> TyFun a (a ~> c) -> Type) Source #
Instance details Defined in Data.Function.Singletons Methods liftSing2 :: forall (x :: b ~> (b ~> c)) (y :: a ~> b). Sing x -> Sing y -> Sing (OnSym2 x y) #
SingI d => SingI1 (OnSym2 d :: (a ~> b) -> TyFun a (a ~> c) -> Type) Source #
Instance details Defined in Data.Function.Singletons Methods liftSing :: forall (x :: a ~> b). Sing x -> Sing (OnSym2 d x) #
(SingI d1, SingI d2) => SingI (OnSym2 d1 d2 :: TyFun a (a ~> c) -> Type) Source #
Instance details Defined in Data.Function.Singletons Methods sing :: Sing (OnSym2 d1 d2) #
SuppressUnusedWarnings (OnSym2 a6989586621679327018 a6989586621679327019 :: TyFun a (a ~> c) -> Type) Source #
Instance details Defined in Data.Function.Singletons Methods suppressUnusedWarnings :: () #
type Apply (OnSym2 a6989586621679327018 a6989586621679327019 :: TyFun a (a ~> c) -> Type) (a6989586621679327020 :: a) Source #
Instance details Defined in Data.Function.Singletons type Apply (OnSym2 a6989586621679327018 a6989586621679327019 :: TyFun a (a ~> c) -> Type) (a6989586621679327020 :: a) = OnSym3 a6989586621679327018 a6989586621679327019 a6989586621679327020

data OnSym3 (a6989586621679327018 :: b ~> (b ~> c)) (a6989586621679327019 :: a ~> b) (a6989586621679327020 :: a) (d :: TyFun a c) infixl 0 Source #

Instances

Instances details

(SingI d1, SingI d2) => SingI1 (OnSym3 d1 d2 :: a -> TyFun a c -> Type) Source #
Instance details Defined in Data.Function.Singletons Methods liftSing :: forall (x :: a). Sing x -> Sing (OnSym3 d1 d2 x) #
SingI d => SingI2 (OnSym3 d :: (a ~> b) -> a -> TyFun a c -> Type) Source #
Instance details Defined in Data.Function.Singletons Methods liftSing2 :: forall (x :: a ~> b) (y :: a). Sing x -> Sing y -> Sing (OnSym3 d x y) #
(SingI d1, SingI d2, SingI d3) => SingI (OnSym3 d1 d2 d3 :: TyFun a c -> Type) Source #
Instance details Defined in Data.Function.Singletons Methods sing :: Sing (OnSym3 d1 d2 d3) #
SuppressUnusedWarnings (OnSym3 a6989586621679327018 a6989586621679327019 a6989586621679327020 :: TyFun a c -> Type) Source #
Instance details Defined in Data.Function.Singletons Methods suppressUnusedWarnings :: () #
type Apply (OnSym3 a6989586621679327018 a6989586621679327019 a6989586621679327020 :: TyFun a c -> Type) (a6989586621679327021 :: a) Source #
Instance details Defined in Data.Function.Singletons type Apply (OnSym3 a6989586621679327018 a6989586621679327019 a6989586621679327020 :: TyFun a c -> Type) (a6989586621679327021 :: a) = On a6989586621679327018 a6989586621679327019 a6989586621679327020 a6989586621679327021

type family OnSym4 (a6989586621679327018 :: b ~> (b ~> c)) (a6989586621679327019 :: a ~> b) (a6989586621679327020 :: a) (a6989586621679327021 :: a) :: c where ... infixl 0 Source #

Equations

OnSym4 (a6989586621679327018 :: b ~> (b ~> c)) (a6989586621679327019 :: a ~> b) (a6989586621679327020 :: a) (a6989586621679327021 :: a) = On a6989586621679327018 a6989586621679327019 a6989586621679327020 a6989586621679327021