| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Data.Extensible.Internal
- data Position xs x
- runPosition :: Position (y : xs) x -> Either (x :~: y) (Position xs x)
- comparePosition :: Position xs x -> Position xs y -> Maybe (x :~: y)
- ord :: Int -> Q Exp
- data Nav xs x where
- navigate :: Position xs x -> Nav xs x
- here :: Position (x : xs) x
- navNext :: Position xs y -> Position (x : xs) y
- navL :: Position (Half xs) y -> Position (x : xs) y
- navR :: Position (Half (Tail xs)) y -> Position (x : xs) y
- class Member xs x where
- membership :: Position xs x
- type (∈) x xs = Member xs x
- data Nat
- class ToInt n where
- type family Lookup x xs :: [Nat]
- type family Succ x :: Nat
- type family MapSucc xs :: [Nat]
- type family Half xs :: [k]
- type family Tail xs :: [k]
- lemmaHalfTail :: Proxy xs -> p (x : Half (Tail xs)) -> p (Half (x : xs))
- type family xs ++ ys :: [k]
- type family Map f xs :: [k]
- type family Merge xs ys :: [k]
- type family Check x xs
- data Expecting a
- data Missing a
- data Ambiguous a
Documentation
The position of x in the type level set xs.
runPosition :: Position (y : xs) x -> Either (x :~: y) (Position xs x) Source
Embodies a type equivalence to ensure that the Position points the first element.
class Member xs x where Source
Member x xs or x ∈ xs indicates that x is an element of xs.
Methods
membership :: Position xs x Source