Safe Haskell | None |
---|---|
Language | Haskell2010 |
- type family (xs :: [u]) !! (n :: Nat) where ...
- type family Length (xs :: [u]) :: Nat where ...
- type family AllF (c :: * -> Constraint) (f :: u -> *) (xs :: [u]) :: Constraint where ...
- type family (as :: [k]) ++ (bs :: [k]) where ...
- type family Replicate (n :: Nat) (x :: u) :: [u] where ...
- data Some f where
- data MaybeSome f
- type family SetAt n xs x where ...
Documentation
type family AllF (c :: * -> Constraint) (f :: u -> *) (xs :: [u]) :: Constraint where ... Source #
AllF c f xs
ensures that constraint c (f x)
holds for all x
in xs
type family Replicate (n :: Nat) (x :: u) :: [u] where ... Source #
Extend a type x
into a type level list xs
of length n
Inductive Natural Numbers
An injective form of Replicate
using inductive Nat'
rather than builtins
The Existential Type Some f
is some f x
where x
is known at runtime