Documentation

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

type (++) (m :: Symbol ) (n :: Symbol ) = AppendSymbol m n infixr 5 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 ( AppendSymbol a b) Source #

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

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

appendAssociates :: forall a b c. Dict ( AppendSymbol ( AppendSymbol a b) c ~ AppendSymbol a ( AppendSymbol 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 ( AppendSymbol ( 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 #