Symbol

data Symbol #

class KnownSymbol (n :: Symbol) #

symbolVal :: KnownSymbol n => proxy n -> String #

symbolVal' :: KnownSymbol n => Proxy# n -> String #

data SomeSymbol where #

someSymbolVal :: String -> SomeSymbol #

sameSymbol :: (KnownSymbol a, KnownSymbol b) => Proxy a -> Proxy b -> Maybe (a :~: b) #

type family AppendSymbol (a :: Symbol) (b :: Symbol) :: Symbol where ... #

type family CmpSymbol (a :: Symbol) (b :: Symbol) :: Ordering where ... #

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

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

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

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

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

appendUnit1 :: Dict (("" ++ a) ~ a) #

appendUnit2 :: Dict ((a ++ "") ~ a) #

appendAssociates :: Dict (((a ++ b) ++ c) ~ (a ++ (b ++ c))) #

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

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

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

lengthSymbol :: KnownSymbol a :- KnownNat (Length a) #

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

take0 :: Dict (Take 0 a ~ "") #

takeEmpty :: Dict (Take n "" ~ "") #

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

drop0 :: Dict (Drop 0 a ~ a) #

dropEmpty :: Dict (Drop n "" ~ "") #

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

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

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

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