Data.Type.List

A type list contains types as elements. We use GADT proofs terms to establish membership and append relations. A Data.Type.List.Map.MapC f is a vector indexed by a type list, where f :: * -> * is applied to each type element.

Documentation

module Data.Type.List.List

Type-level nil, cons, and ++

module Data.Type.List.Map

Vectors parameterized by a * -> * and indexed by a type list

module Data.Type.List.Proof.Member

Membership functions and proofs

module Data.Type.List.Proof.Append

Append functions and proofs

module Data.Type.Equality

module Data.Proxy