Module type_equalities::type_functions [−][src]
Expand description
TypeFunctions have the amazing property that they can be used to push the equality of a
type-level argument through to an equality of the type-level result.
In this crate, helper structs are defined that implement TypeFunction with various resulting
types. These structs are then supposed to be passed to substitute, TypeEq::substitute
and TypeEq::lift_through.
Example
let eq: TypeEq<&u32, &u32> = refl::<u32>().lift_through::<RefF<'_>>();Structs
allocThe TypeFunction ApF<BoxF, A> == Box<A>
Composition for TypeFunctions, i.e. ApF<ComposeF<F, G>, T> == ApF<F, ApF<G, T>>
The identity TypeFunction, ApF<IdF, T> == T. Coercing through this gives
us the basic safe transmute.
A TypeFunction version of the Martin-Löf identity type:
ApF<LoefIdF<T>, U> == TypeEq<T, U>.
LoefIdF flipped, i.e. ApF<LoefIdFlippedF<T>, U> == TypeEq<U, T>
The TypeFunction ApF<MutRefF<'a>, A> == &'a mut A
The TypeFunction ApF<RefF<'a>, A> == &'a A
The TypeFunction ApF<SliceF<N>, A> == [A; N]
Traits
A trait for type level functions, mapping type arguments to type results.
Type Definitions
The result of applying the TypeFunction F to T.