vinyl-0.3: Extensible Records

Data.Vinyl.Witnesses

Synopsis

class Implicit p whereSource

Methods

implicitly :: pSource

Instances

data Elem whereSource

An inductive list membership proposition.

Constructors

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.

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

A constraint for implicit resolution of list subset proofs.