witness-0.7: values that witness types
Safe HaskellNone
LanguageGHC2021

Data.Type.Witness.Specific.ApplyStack

Documentation

type family ApplyStack (f :: [k -> k]) (a :: k) :: k where ... Source #

Equations

ApplyStack ('[] :: [k -> k]) (a :: k) = a 
ApplyStack (t ': tt :: [k -> k]) (a :: k) = t (ApplyStack tt a) 

witApplyConcatRefl :: forall k (f1 :: [k -> k]) (f2 :: [k -> k]) (a :: k) (w :: (k -> k) -> Type). ListType w f1 -> ApplyStack (Concat f1 f2) a :~: ApplyStack f1 (ApplyStack f2 a) Source #

applyConcatRefl :: forall k (f1 :: [k -> k]) (f2 :: [k -> k]) (a :: k) (w :: (k -> k) -> Type). Is (ListType w) f1 => ApplyStack (Concat f1 f2) a :~: ApplyStack f1 (ApplyStack f2 a) Source #