[−][src]Enum chalk_ir::QuantifierKind
Kinds of quantifiers in the logic, such as forall
and exists
.
Variants
Universal quantifier ForAll
.
A formula with the universal quantifier forall(x). P(x)
is satisfiable
if and only if the subformula P(x)
is true for all possible values for x.
Existential quantifier Exists
.
A formula with the existential quantifier exists(x). P(x)
is satisfiable
if and only if there exists at least one value for all possible values of x
which satisfies the subformula P(x)
.
In the context of chalk, the existential quantifier usually demands the
existence of exactly one instance (i.e. type) that satisfies the formula
(i.e. type constraints). More than one instance means that the result is ambiguous.
Trait Implementations
impl Clone for QuantifierKind
[src]
fn clone(&self) -> QuantifierKind
[src]
fn clone_from(&mut self, source: &Self)
1.0.0[src]
impl Copy for QuantifierKind
[src]
impl Debug for QuantifierKind
[src]
impl Eq for QuantifierKind
[src]
impl<I: Interner, TI: TargetInterner<I>> Fold<I, TI> for QuantifierKind
[src]
type Result = Self
The type of value that will be produced once folding is done. Typically this is Self
, unless Self
contains borrowed values, in which case owned values are produced (for example, one can fold over a &T
value where T: Fold
, in which case you get back a T
, not a &T
). Read more
fn fold_with<'i>(
&self,
_folder: &mut dyn Folder<'i, I, TI>,
_outer_binder: DebruijnIndex
) -> Fallible<Self::Result> where
I: 'i,
TI: 'i,
[src]
&self,
_folder: &mut dyn Folder<'i, I, TI>,
_outer_binder: DebruijnIndex
) -> Fallible<Self::Result> where
I: 'i,
TI: 'i,
impl Hash for QuantifierKind
[src]
fn hash<__H: Hasher>(&self, state: &mut __H)
[src]
fn hash_slice<H>(data: &[Self], state: &mut H) where
H: Hasher,
1.3.0[src]
H: Hasher,
impl Ord for QuantifierKind
[src]
fn cmp(&self, other: &QuantifierKind) -> Ordering
[src]
#[must_use]fn max(self, other: Self) -> Self
1.21.0[src]
#[must_use]fn min(self, other: Self) -> Self
1.21.0[src]
#[must_use]fn clamp(self, min: Self, max: Self) -> Self
[src]
impl PartialEq<QuantifierKind> for QuantifierKind
[src]
fn eq(&self, other: &QuantifierKind) -> bool
[src]
#[must_use]fn ne(&self, other: &Rhs) -> bool
1.0.0[src]
impl PartialOrd<QuantifierKind> for QuantifierKind
[src]
fn partial_cmp(&self, other: &QuantifierKind) -> Option<Ordering>
[src]
#[must_use]fn lt(&self, other: &Rhs) -> bool
1.0.0[src]
#[must_use]fn le(&self, other: &Rhs) -> bool
1.0.0[src]
#[must_use]fn gt(&self, other: &Rhs) -> bool
1.0.0[src]
#[must_use]fn ge(&self, other: &Rhs) -> bool
1.0.0[src]
impl StructuralEq for QuantifierKind
[src]
impl StructuralPartialEq for QuantifierKind
[src]
impl<I: Interner> Visit<I> for QuantifierKind
[src]
fn visit_with<'i, R: VisitResult>(
&self,
_visitor: &mut dyn Visitor<'i, I, Result = R>,
_outer_binder: DebruijnIndex
) -> R where
I: 'i,
[src]
&self,
_visitor: &mut dyn Visitor<'i, I, Result = R>,
_outer_binder: DebruijnIndex
) -> R where
I: 'i,
impl<I: Interner> Zip<I> for QuantifierKind
[src]
Auto Trait Implementations
impl RefUnwindSafe for QuantifierKind
impl Send for QuantifierKind
impl Sync for QuantifierKind
impl Unpin for QuantifierKind
impl UnwindSafe for QuantifierKind
Blanket Implementations
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> Cast for T
[src]
fn cast<U>(self, interner: &U::Interner) -> U where
Self: CastTo<U>,
U: HasInterner,
[src]
Self: CastTo<U>,
U: HasInterner,
impl<T> From<T> for T
[src]
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<T, I> Shift<I> for T where
I: Interner,
T: Fold<I, I>,
[src]
I: Interner,
T: Fold<I, I>,
fn shifted_in(&Self, &I) -> <T as Fold<I, I>>::Result
[src]
fn shifted_in_from(&Self, &I, DebruijnIndex) -> <T as Fold<I, I>>::Result
[src]
fn shifted_out_to(
&Self,
&I,
DebruijnIndex
) -> Result<<T as Fold<I, I>>::Result, NoSolution>
[src]
&Self,
&I,
DebruijnIndex
) -> Result<<T as Fold<I, I>>::Result, NoSolution>
fn shifted_out(&Self, &I) -> Result<<T as Fold<I, I>>::Result, NoSolution>
[src]
impl<T> ToOwned for T where
T: Clone,
[src]
T: Clone,
type Owned = T
The resulting type after obtaining ownership.
fn to_owned(&self) -> T
[src]
fn clone_into(&self, target: &mut T)
[src]
impl<T, U> TryFrom<U> for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,
type Error = <U as TryFrom<T>>::Error
The type returned in the event of a conversion error.
fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>
[src]
impl<T, I> VisitExt<I> for T where
I: Interner,
T: Visit<I>,
[src]
I: Interner,
T: Visit<I>,