Type Definition prop::hooo::Pow

pub type Pow<A, B> = fn(_: B) -> A;

a^b.

Trait Implementations

impl<A: DProp, B: DProp> Decidable for Pow<A, B>

fn decide() -> ExcM<Self>

Get excluded middle rule.

impl<A: Prop, B: Prop> PowExt<A, B> for Pow<B, A>

fn trans<C: Prop>(&self, f: Pow<C, B>) -> Pow<C, A>

Transitivity.

fn lift<C: Prop>(&self) -> Pow<Self, C>

Lift.