Data.Vinyl.Witnesses

Documentation

class Implicit p where

Methods

implicitly :: p

Instances

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

Implicit (Elem k x ((:) k x xs))

data Elem :: k -> [k] -> * 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.

type (∈) x xs = IElem x xs