Moduleconstraints-0.14.4Haskell2010

Data.Constraint.Symbol

Utilities for working with KnownSymbol constraints.

familytype family AppendSymbol (a :: Symbol) (b :: Symbol) :: Symbol

Concatenation of type-level symbols.

typetype (++) (m :: Symbol) (n :: Symbol) = AppendSymbol m n

An infix synonym for AppendSymbol.

familytype family Take :: Nat -> Symbol -> Symbol where

familytype family Drop :: Nat -> Symbol -> Symbol where

familytype family Length :: Symbol -> Nat where

valueappendSymbol :: (KnownSymbol a, KnownSymbol b) :- KnownSymbol (AppendSymbol a b)

valueappendUnit1 :: Dict (AppendSymbol "" a ~ a)

valueappendUnit2 :: Dict (AppendSymbol a "" ~ a)

valueappendAssociates :: Dict (AppendSymbol (AppendSymbol a b) c ~ AppendSymbol a (AppendSymbol b c))

valuetakeSymbol :: (KnownNat n, KnownSymbol a) :- KnownSymbol (Take n a)

valuedropSymbol :: (KnownNat n, KnownSymbol a) :- KnownSymbol (Drop n a)

valuetakeAppendDrop :: Dict (AppendSymbol (Take n a) (Drop n a) ~ a)

valuelengthSymbol :: KnownSymbol a :- KnownNat (Length a)

valuetakeLength :: (Length a <= n) :- (Take n a ~ a)

valuetake0 :: Dict (Take 0 a ~ "")

valuetakeEmpty :: Dict (Take n "" ~ "")

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

valuedrop0 :: Dict (Drop 0 a ~ a)

valuedropEmpty :: Dict (Drop n "" ~ "")

valuelengthTake :: Dict (Length (Take n a) <= n)

valuelengthDrop :: Dict (Length a <= (Length (Drop n a) + n))

valuedropDrop :: Dict (Drop n (Drop m a) ~ Drop (n + m) a)

valuetakeTake :: Dict (Take n (Take m a) ~ Take (Min n m) a)