Data.Constraint.Symbol

Utilities for working with KnownSymbol constraints.

Documentation

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

Concatenation of type-level symbols.

Since: base-4.10.0.0

type (++) (m :: Symbol) (n :: Symbol) = AppendSymbol m n infixr 5

An infix synonym for AppendSymbol.

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 (AppendSymbol a b)

appendUnit1 :: forall a. Dict (AppendSymbol "" a ~ a)

appendUnit2 :: forall a. Dict (AppendSymbol a "" ~ a)

appendAssociates :: forall a b c. Dict (AppendSymbol (AppendSymbol a b) c ~ AppendSymbol a (AppendSymbol b c))

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

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

takeAppendDrop :: forall n a. Dict (AppendSymbol (Take n a) (Drop n a) ~ a)

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

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

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

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

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

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

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

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

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

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

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