Documentation

type family (++) :: Symbol -> Symbol -> Symbol where ... Source #

type family Take :: Nat -> Symbol -> Symbol where ... Source #

type family Drop :: Nat -> Symbol -> Symbol where ... Source #

type family Length :: Symbol -> Nat where ... Source #

appendSymbol :: (KnownSymbol a, KnownSymbol b) :- KnownSymbol (a ++ b) Source #

appendUnit1 :: forall a. Dict (("" ++ a) ~ a) Source #

appendUnit2 :: forall a. Dict ((a ++ "") ~ a) Source #

appendAssociates :: forall a b c. Dict (((a ++ b) ++ c) ~ (a ++ (b ++ c))) Source #

takeSymbol :: forall n a. (KnownNat n, KnownSymbol a) :- KnownSymbol (Take n a) Source #

dropSymbol :: forall n a. (KnownNat n, KnownSymbol a) :- KnownSymbol (Drop n a) Source #

takeAppendDrop :: forall n a. Dict ((Take n a ++ Drop n a) ~ a) Source #

lengthSymbol :: forall a. KnownSymbol a :- KnownNat (Length a) Source #

takeLength :: forall n a. (Length a <= n) :- (Take n a ~ a) Source #

take0 :: forall a. Dict (Take 0 a ~ "") Source #

takeEmpty :: forall n. Dict (Take n "" ~ "") Source #

dropLength :: forall n a. (Length a <= n) :- (Drop n a ~ "") Source #

drop0 :: forall a. Dict (Drop 0 a ~ a) Source #

dropEmpty :: forall n. Dict (Drop n "" ~ "") Source #

lengthTake :: forall n a. Dict (Length (Take n a) <= n) Source #

lengthDrop :: forall n a. Dict (Length a <= (Length (Drop n a) + n)) Source #

dropDrop :: forall n m a. Dict (Drop n (Drop m a) ~ Drop (n + m) a) Source #

takeTake :: forall n m a. Dict (Take n (Take m a) ~ Take (Min n m) a) Source #