Module type_equalities::type_functions [−][src]
Expand description
TypeFunction
s 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
alloc
The TypeFunction
ApF<BoxF, A> == Box<A>
Composition for TypeFunction
s, 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
.