Data.Type.List.Proof.Member

Proofs regarding membership of a type in a type list.

Abstract data types

data Member ctx a where

A Member ctx a is a "proof" that the type a is in the type list ctx, meaning that ctx equals

  t0 ':>' a ':>' t1 ':>' ... ':>' tn

for some types t0,t1,...,tn.

Constructors

Member_Base :: Member (ctx :> a) a

Member_Step :: Member ctx a -> Member (ctx :> b) a

Instances

Typeable2 Member

Show (Member r a)

Liftable (Member c a)

Operators on Member proofs

toEq :: Member (Nil :> a) b -> b :=: a

weakenL :: Proxy r1 -> Member r2 a -> Member (r1 :++: r2) a

same :: Member r a -> Member r b -> Maybe (a :=: b)

weakenR :: Member r1 a -> Append r1 r2 r -> Member r a

split :: Append r1 r2 r -> Member r a -> Either (Member r1 a) (Member r2 a)