| Copyright | (c) Fumiaki Kinoshita 2015 |
|---|---|
| License | BSD3 |
| Maintainer | Fumiaki Kinoshita <[email protected]> |
| Stability | experimental |
| Portability | non-portable |
| Safe Haskell | None |
| Language | Haskell2010 |
Data.Extensible.Inclusion
Description
- data Position xs x
- runPosition :: Position (y : xs) x -> Either (x :~: y) (Position xs x)
- type (∈) x xs = Member xs x
- class Member xs x where
- membership :: Position xs x
- data Expecting a
- data Missing a
- data Ambiguous a
- ord :: Int -> Q Exp
- type (⊆) xs ys = Include ys xs
- type Include ys = Forall (Member ys)
- inclusion :: forall xs ys. Include ys xs => Position ys :* xs
- shrink :: xs ⊆ ys => (h :* ys) -> h :* xs
- spread :: xs ⊆ ys => (h :| xs) -> h :| ys
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