singLength :: Sing ns -> Length ns Source #

singProd :: Sing as -> Prod Sing as Source #

prodSing :: Prod Sing as -> Sing as Source #

splitSing :: Length ns -> Sing (ns ++ ms) -> (Sing ns, Sing ms) Source #

takeSing :: Length ns -> Length ms -> Sing (ns ++ ms) -> Sing ns Source #

singProdNat :: forall as. Sing as -> Prod Nat as Source #

entailNat :: forall n. SingI n :- Known Nat n Source #

singSings :: forall ns. SingI ns :- ListC (SingI <$> ns) Source #

witSings :: forall ns. Sing ns -> Wit (ListC (SingI <$> ns)) Source #

entailEvery :: forall as f. (forall a. SingI a :- f a) -> SingI as :- Every f as Source #

singUniform :: Uniform a (b ': bs) -> SingI b :- SingI a Source #

entailSing :: forall a b. (Sing a -> Sing b) -> SingI a :- SingI b Source #

entailSing2 :: forall a b c. (Sing a -> Sing b -> Sing c) -> (SingI a, SingI b) :- SingI c Source #

singWit :: forall a p q t. (p, Witness p q t) => (Sing a -> t) -> SingI a :- q Source #

(%:++) :: Sing as -> Sing bs -> Sing (as ++ bs) infixr 5 Source #

sReverse :: Sing as -> Sing (Reverse as) Source #

sSnoc :: Sing as -> Sing a -> Sing (as >: a) Source #

sOnly :: Sing a -> Sing '[a] Source #

replicateSing :: Sing a -> Nat n -> Sing (Replicate n a) Source #