Struct prop::path_semantics::POrdProof
source · [−]pub struct POrdProof<T, U>(_);
Expand description
Proof of path semantical order.
Implementations
sourceimpl<T, U> POrdProof<T, U>
impl<T, U> POrdProof<T, U>
sourcepub fn transitivity<V>(self, _: POrdProof<U, V>) -> POrdProof<T, V>
pub fn transitivity<V>(self, _: POrdProof<U, V>) -> POrdProof<T, V>
Transivity of path semantical order.
sourcepub fn by_eq_left<V>(self, eq: Eq<T, V>) -> POrdProof<V, U>
pub fn by_eq_left<V>(self, eq: Eq<T, V>) -> POrdProof<V, U>
Transform left argument by equivalence.
sourcepub fn by_eq_right<V>(self, eq: Eq<U, V>) -> POrdProof<T, V>
pub fn by_eq_right<V>(self, eq: Eq<U, V>) -> POrdProof<T, V>
Transform right argument by equivalence.
sourcepub fn by_imply_left<V>(self, _: Imply<V, T>) -> POrdProof<V, U>
pub fn by_imply_left<V>(self, _: Imply<V, T>) -> POrdProof<V, U>
Transform left argument by implication.
sourcepub fn by_imply_right<V>(self, _: Imply<U, V>) -> POrdProof<T, V>
pub fn by_imply_right<V>(self, _: Imply<U, V>) -> POrdProof<T, V>
Transform right argument by implication.
sourcepub fn merge_right<V>(self, _: POrdProof<T, V>) -> POrdProof<T, And<U, V>>
pub fn merge_right<V>(self, _: POrdProof<T, V>) -> POrdProof<T, And<U, V>>
Merges two proofs of order at right side.
sourcepub fn merge_left<V>(self, _: POrdProof<V, U>) -> POrdProof<And<T, V>, U>
pub fn merge_left<V>(self, _: POrdProof<V, U>) -> POrdProof<And<T, V>, U>
Merges two proofs of order at left side.
sourcepub fn and<T2, U2>(
self,
_: POrdProof<T2, U2>
) -> POrdProof<And<T, T2>, And<U, U2>>
pub fn and<T2, U2>(
self,
_: POrdProof<T2, U2>
) -> POrdProof<And<T, T2>, And<U, U2>>
Combine two proofs into one using AND.
Trait Implementations
impl<T: Copy, U: Copy> Copy for POrdProof<T, U>
Auto Trait Implementations
impl<T, U> RefUnwindSafe for POrdProof<T, U> where
T: RefUnwindSafe,
U: RefUnwindSafe,
impl<T, U> Send for POrdProof<T, U> where
T: Send,
U: Send,
impl<T, U> Sync for POrdProof<T, U> where
T: Sync,
U: Sync,
impl<T, U> Unpin for POrdProof<T, U> where
T: Unpin,
U: Unpin,
impl<T, U> UnwindSafe for POrdProof<T, U> where
T: UnwindSafe,
U: UnwindSafe,
Blanket Implementations
sourceimpl<T> BorrowMut<T> for T where
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
const: unstable · sourcefn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more
sourceimpl<T> Existential for T where
T: Decidable,
impl<T> Existential for T where
T: Decidable,
sourceimpl<T> ToOwned for T where
T: Clone,
impl<T> ToOwned for T where
T: Clone,
type Owned = T
type Owned = T
The resulting type after obtaining ownership.
sourcefn clone_into(&self, target: &mut T)
fn clone_into(&self, target: &mut T)
🔬 This is a nightly-only experimental API. (
toowned_clone_into
)Uses borrowed data to replace owned data, usually by cloning. Read more