vinyl-0.3: Extensible Records

Safe HaskellNone

Data.Vinyl.Witnesses

Synopsis

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)) 

data Elem whereSource

An inductive list membership proposition.

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 IElem x xs = Implicit (Elem x xs)Source

A constraint for implicit resolution of list membership proofs.

data Subset whereSource

An inductive list subset relation.

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) 

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

A constraint for implicit resolution of list subset proofs.