Data.Extensible.Internal

Documentation

data Position xs x

The position of x in the type level set xs.

Instances

Typeable ([k] -> k -> *) (Position k)

Eq (Position k xs x)

Ord (Position k xs x)

Show (Position k xs x)

runPosition :: Position (y : xs) x -> Either (x :~: y) (Position xs x)

Embodies a type equivalence to ensure that the Position points the first element.

comparePosition :: Position xs x -> Position xs y -> Maybe (x :~: y)

ord :: Int -> Q Exp

data Nav xs x where

Constructors

Here :: Nav (x : xs) x

NavL :: Position (Half xs) x -> Nav (e : xs) x

NavR :: Position (Half (Tail xs)) x -> Nav (e : xs) x

navigate :: Position xs x -> Nav xs x

here :: Position (x : xs) x

navL :: Position (Half xs) y -> Position (x : xs) y

navR :: Position (Half (Tail xs)) y -> Position (x : xs) y

class Member xs x where

Member x xs or x ∈ xs indicates that x is an element of xs.

Methods

membership :: Position xs x

Instances

Record Nat (Lookup k x xs) => Member k xs x

type (∈) x xs = Member xs x

Unicode flipped alias for Member

data Nat

Constructors

Zero

DNat Nat

SDNat Nat

NotFound

Instances

Record Nat Zero

Record Nat n => Record Nat (SDNat n)

Record Nat n => Record Nat (DNat n)

class Record n where

Methods

theInt :: Proxy n -> Int

Instances

Record Nat Zero

Record Nat n => Record Nat (SDNat n)

Record Nat n => Record Nat (DNat n)

type family Lookup x xs :: Nat

Equations

Lookup x (x : xs) = Zero

Lookup x (y : ys) = Succ (Lookup x ys)

Lookup x [] = NotFound

type family Succ x :: Nat

Equations

Succ Zero = SDNat Zero

Succ (DNat n) = SDNat n

Succ (SDNat n) = DNat (Succ n)

Succ NotFound = NotFound

type family Half xs :: [k]

Equations

Half [] = []

Half (x : (y : zs)) = x : zs

Half (x : []) = x : []

type family Tail xs :: [k]

Equations

Tail (x : xs) = xs

Tail [] = []

lemmaHalfTail :: Proxy xs -> p (x : Half (Tail xs)) -> p (Half (x : xs))