vinyl-0.1.1.0: Extensible Records

Safe HaskellNone

Data.Vinyl.Witnesses

Documentation

class Implicit p whereSource

Methods

implicitly :: pSource

Instances

(IElem k x ys, ISubset k xs ys) => Implicit (Subset k (: k x xs) ys) 
Implicit (Subset k ([] k) xs) 
Implicit (Elem k x xs) => Implicit (Elem k x (: k y xs)) 
Implicit (Elem k x (: k x xs)) 

type IElem x xs = Implicit (Elem x xs)Source

data Elem whereSource

Constructors

Here :: Elem x (x : xs) 
There :: Elem x xs -> Elem x (y : xs) 

Instances

Implicit (Elem k x xs) => Implicit (Elem k x (: k y xs)) 
Implicit (Elem k x (: k x xs)) 

type ISubset xs ys = Implicit (Subset xs ys)Source

data Subset whereSource

Constructors

SubsetNil :: Subset `[]` xs 
SubsetCons :: Elem x ys -> Subset xs ys -> Subset (x : xs) ys 

Instances

(IElem k x ys, ISubset k xs ys) => Implicit (Subset k (: k x xs) ys) 
Implicit (Subset k ([] k) xs)