Trait identity::Identity [−] [src]

pub trait Identity<A: ?Sized, B: ?Sized>: Sized {
    type Inverse: Identity<B, A, Inverse=Self>;
    fn conv(&self, x: A) -> B where A: Sized, B: Sized;
    fn conv_ref<'a>(&self, x: &'a A) -> &'a B;
    fn conv_mut<'a>(&self, x: &'a mut A) -> &'a mut B;
    fn conv_box(&self, x: Box<A>) -> Box<B>;
    fn conv_under<TF: TyFun<A> + TyFun<B>>(&self, x: TF::Result) -> TF::Result where TF::Result: Sized, TF::Result: Sized;
    fn inv(&self) -> &Self::Inverse;
    fn elim<Prop: TysFun<TyPair<A, Refl<A>>> + TysFun<TyPair<B, Self>>>(&self, refl_case: Prop::Result) -> Prop::Result where Prop::Result: Sized, Prop::Result: Sized;
    fn elim_alt<Prop: TysFun<TyTriple<A, B, Self>>, ReflCase: Forall<AndThen<MLReflCase, Uncurry<Prop>>>>(&self, refl_case: ReflCase) -> Prop::Result where Prop::Result: Sized;
}

An identity type; that is, the type bound of “equality witnesses.”

Associated Types

type Inverse: Identity<B, A, Inverse=Self>

Required Methods

fn conv(&self, x: A) -> B where A: Sized, B: Sized

fn conv_ref<'a>(&self, x: &'a A) -> &'a B

fn conv_mut<'a>(&self, x: &'a mut A) -> &'a mut B

fn conv_box(&self, x: Box<A>) -> Box<B>

fn conv_under<TF: TyFun<A> + TyFun<B>>(&self, x: TF::Result) -> TF::Result where TF::Result: Sized, TF::Result: Sized

Leibniz's identity rule, approximately.

fn inv(&self) -> &Self::Inverse

fn elim<Prop: TysFun<TyPair<A, Refl<A>>> + TysFun<TyPair<B, Self>>>(&self, refl_case: Prop::Result) -> Prop::Result where Prop::Result: Sized, Prop::Result: Sized

Paulin-Mohring's J rule, approximately.

fn elim_alt<Prop: TysFun<TyTriple<A, B, Self>>, ReflCase: Forall<AndThen<MLReflCase, Uncurry<Prop>>>>(&self, refl_case: ReflCase) -> Prop::Result where Prop::Result: Sized

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

Implementors