Data.Vinyl.Witnesses

Documentation

class Implicit p where

Methods

implicitly :: p

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 where

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)

A constraint for implicit resolution of list membership proofs.

data Subset where

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)

A constraint for implicit resolution of list subset proofs.