Struct identity::Refl

pub struct Refl<A: ?Sized> {
    // some fields omitted
}

Trait Implementations

impl<A: ?Sized> Debug for Refl<A>

fn fmt(&self, fmtr: &mut Formatter) -> Result

Formats the value using the given formatter.

impl<A: ?Sized> Clone for Refl<A>

fn clone(&self) -> Refl<A>

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<A: ?Sized> Copy for Refl<A>

impl<A: ?Sized> Default for Refl<A>

fn default() -> Refl<A>

Returns the "default value" for a type.

impl<A: ?Sized> Hash for Refl<A>

fn hash<H: Hasher>(&self, hshr: &mut H)

Feeds this value into the state given, updating the hasher as necessary.

fn hash_slice<H>(data: &[Self], state: &mut H) where H: Hasher

Feeds a slice of this type into the state provided.

impl<A: ?Sized> Identity<A, A> for Refl<A>

type Inverse = Self

fn conv(&self, x: A) -> A where 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

Leibniz's identity rule, approximately.

fn elim<Prop: TysFun<TyPair<A, Refl<A>>>>(&self, refl_case: Prop::Result) -> Prop::Result where Prop::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::Result where Prop::Result: Sized

Martin-Löf's J rule, approximately.