type-settheory-0.1.2: Type-level sets and functions expressed as types Source code Contents Index

Type.Dummies

Synopsis

data Lower a data Lower1 a where LowerElement :: u x -> Lower1 u (Lower x) data Lower2 a where Lower1Element :: u x -> Lower2 u (Lower1 x) data Lower3 a where Lower2Element :: u x -> Lower3 u (Lower2 x) data PAIR a b x data PAIR1 a b x data PAIR2 a b x data PAIR3 a b x

Documentation

data Lower a Source

"Kind-cast" (* -> *) to *

data Lower1 a where Source

"Kind-cast" ((* -> *) -> *) to (* -> *) . Also lower elements using Lower. Constructors LowerElement :: u x -> Lower1 u (Lower x) Instances (Lower f ~ lf, Fact ((dom :~>: cod) f)) => Fact ((dom :~~>: cod) lf)

data Lower2 a where Source

"Kind-cast" (((* -> *) -> *) -> *) to ((* -> *) -> *) . Also lower elements using Lower1. Constructors Lower1Element :: u x -> Lower2 u (Lower1 x)

data Lower3 a where Source

"Kind-cast" ((((* -> *) -> *) -> *) -> *) to (((* -> *) -> *) -> *) . Also lower elements using Lower2. Constructors Lower2Element :: u x -> Lower3 u (Lower2 x)

data PAIR a b x Source

Pair of types of kind (* -> *)

data PAIR1 a b x Source

Pair of types of kind ((* -> *) -> *)

data PAIR2 a b x Source

Pair of types of kind (((* -> *) -> *) -> *)

data PAIR3 a b x Source

Pair of types of kind ((((* -> *) -> *) -> *) -> *)

Produced by Haddock version 2.4.2