vinyl-0.4.1: Extensible Records

Data.Vinyl.Witnesses

Synopsis

class Implicit p where Source

Methods

implicitly :: p Source

Instances

data Elem :: k -> [k] -> * where Source

An inductive list membership proposition.

Constructors

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

A constraint for implicit resolution of list membership proofs.

type (∈) x xs = IElem x xs Source