Safe Haskell	None
Language	Haskell2010

Data.Vinyl.TypeLevel

Synopsis

Documentation

A mere approximation of the natural numbers. And their image as lifted by -XDataKinds corresponds to the actual natural numbers.

Constructors

Z
S !Nat

Instances

RSubset k ([] k) ss ([] Nat)
(RElem k r ss i, RSubset k rs ss is) => RSubset k ((:) k r rs) ss ((:) Nat i is)

type family RIndex r rs :: Nat Source

A partial relation that gives the index of a value in a list.

Equations

RIndex r (r : rs) = Z
RIndex r (s : rs) = S (RIndex r rs)

type family RImage rs ss :: [Nat] Source

A partial relation that gives the indices of a sublist in a larger list.

Equations

RImage [] ss = []
RImage (r : rs) ss = RIndex r ss : RImage rs ss

type family RecAll f rs c :: Constraint Source

A constraint-former which applies to every field in a record.

Equations

RecAll f [] c = ()
RecAll f (r : rs) c = (c (f r), RecAll f rs c)

type family as ++ bs :: [k] Source

Append for type-level lists.

Equations

[] ++ bs = bs
(a : as) ++ bs = a : (as ++ bs)