Data.Extensible.Internal

data Membership xs x

getMemberId

runMembership

compareMembership

ord

data NavHere xs x

navigate

here

navNext

navL

navR

data h :* s

class Member xs x

type x ∈ xs

data Nat

class ToInt n

type family Lookup x xs :: [Nat]

type family ListIndex n xs :: k

class LookupTree n xs x

type family Succ x :: Nat

type family MapSucc xs :: [Nat]

type family Pred n :: Nat

type family Div2 n :: Nat

type family Half xs :: [k]

type family Head xs :: k

type family Tail xs :: [k]

lemmaHalfTail

lemmaMerging

type family xs ++ ys :: [k]

type family Map f xs :: [k]

type family Merge xs ys :: [k]

type family Concat xs :: [k]

type family Check x xs

data Expecting a

data Missing a

data Ambiguous a