Struct identity::Refl
[−]
[src]
pub struct Refl<A: ?Sized> { /* fields omitted */ }
Trait Implementations
impl<A: ?Sized> Debug for Refl<A>
[src]
impl<A: ?Sized> Clone for Refl<A>
[src]
fn clone(&self) -> Refl<A>
Returns a copy of the value. Read more
fn clone_from(&mut self, source: &Self)
1.0.0
Performs copy-assignment from source
. Read more
impl<A: ?Sized> Copy for Refl<A>
[src]
impl<A: ?Sized> Default for Refl<A>
[src]
impl<A: ?Sized> Hash for Refl<A>
[src]
fn hash<H: Hasher>(&self, hshr: &mut H)
Feeds this value into the given [Hasher
]. Read more
fn hash_slice<H>(data: &[Self], state: &mut H) where
H: Hasher,
1.3.0
H: Hasher,
Feeds a slice of this type into the given [Hasher
]. Read more
impl<A: ?Sized> Identity<A, A> for Refl<A>
[src]
type Inverse = Self
fn conv(&self, x: A) -> A where
A: Sized,
A: Sized,
fn conv_ref<'a>(&self, x: &'a A) -> &'a A
fn conv_mut<'a>(&self, x: &'a mut A) -> &'a mut A
fn conv_box(&self, x: Box<A>) -> Box<A>
fn inv(&self) -> &Self
fn conv_under<TF: TyFun<A>>(&self, x: TF::Result) -> TF::Result where
TF::Result: Sized,
TF::Result: Sized,
Leibniz's identity rule, approximately.
fn elim<Prop: TysFun<TyPair<A, Refl<A>>>>(
&self,
refl_case: <Prop as TysFun<TyPair<A, Refl<A>>>>::Result
) -> <Prop as TysFun<TyPair<A, Refl<A>>>>::Result where
<Prop as TysFun<TyPair<A, Refl<A>>>>::Result: Sized,
&self,
refl_case: <Prop as TysFun<TyPair<A, Refl<A>>>>::Result
) -> <Prop as TysFun<TyPair<A, Refl<A>>>>::Result where
<Prop as TysFun<TyPair<A, Refl<A>>>>::Result: Sized,
Paulin-Mohring's J rule, approximately.
fn elim_alt<Prop: TysFun<TyTriple<A, A, Refl<A>>>, ReflCase: Forall<AndThen<MLReflCase, Uncurry<Prop>>>>(
&self,
refl_case: ReflCase
) -> <Prop as TysFun<TyTriple<A, A, Refl<A>>>>::Result where
<Prop as TysFun<TyTriple<A, A, Refl<A>>>>::Result: Sized,
&self,
refl_case: ReflCase
) -> <Prop as TysFun<TyTriple<A, A, Refl<A>>>>::Result where
<Prop as TysFun<TyTriple<A, A, Refl<A>>>>::Result: Sized,
Martin-Löf's J rule, approximately.