# Enum chalk_ir::QuantifierKind

source · ```
pub enum QuantifierKind {
ForAll,
Exists,
}
```

## Expand description

Kinds of quantifiers in the logic, such as `forall`

and `exists`

.

## Variants§

### ForAll

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.

### Exists

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§

source§### impl Clone for QuantifierKind

### impl Clone for QuantifierKind

source§#### fn clone(&self) -> QuantifierKind

#### fn clone(&self) -> QuantifierKind

Returns a copy of the value. Read more

1.0.0 · source§#### fn clone_from(&mut self, source: &Self)

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

Performs copy-assignment from

`source`

. Read moresource§### impl Debug for QuantifierKind

### impl Debug for QuantifierKind

source§### impl Hash for QuantifierKind

### impl Hash for QuantifierKind

source§### impl Ord for QuantifierKind

### impl Ord for QuantifierKind

source§#### fn cmp(&self, other: &QuantifierKind) -> Ordering

#### fn cmp(&self, other: &QuantifierKind) -> Ordering

1.21.0 · source§#### fn max(self, other: Self) -> Selfwhere
Self: Sized,

#### fn max(self, other: Self) -> Selfwhere Self: Sized,

Compares and returns the maximum of two values. Read more

source§### impl PartialEq<QuantifierKind> for QuantifierKind

### impl PartialEq<QuantifierKind> for QuantifierKind

source§#### fn eq(&self, other: &QuantifierKind) -> bool

#### fn eq(&self, other: &QuantifierKind) -> bool

This method tests for

`self`

and `other`

values to be equal, and is used
by `==`

.source§### impl PartialOrd<QuantifierKind> for QuantifierKind

### impl PartialOrd<QuantifierKind> for QuantifierKind

source§#### fn partial_cmp(&self, other: &QuantifierKind) -> Option<Ordering>

#### fn partial_cmp(&self, other: &QuantifierKind) -> Option<Ordering>

1.0.0 · source§#### fn le(&self, other: &Rhs) -> bool

#### fn le(&self, other: &Rhs) -> bool

This method tests less than or equal to (for

`self`

and `other`

) and is used by the `<=`

operator. Read moresource§### impl<I: Interner> TypeFoldable<I> for QuantifierKind

### impl<I: Interner> TypeFoldable<I> for QuantifierKind

source§#### fn try_fold_with<E>(
self,
_folder: &mut dyn FallibleTypeFolder<I, Error = E>,
_outer_binder: DebruijnIndex
) -> Result<Self, E>

#### fn try_fold_with<E>( self, _folder: &mut dyn FallibleTypeFolder<I, Error = E>, _outer_binder: DebruijnIndex ) -> Result<Self, E>

Apply the given folder

`folder`

to `self`

; `binders`

is the
number of binders that are in scope when beginning the
folder. Typically `binders`

starts as 0, but is adjusted when
we encounter `Binders<T>`

in the IR or other similar
constructs.source§#### fn fold_with(
self,
folder: &mut dyn TypeFolder<I>,
outer_binder: DebruijnIndex
) -> Self

#### fn fold_with( self, folder: &mut dyn TypeFolder<I>, outer_binder: DebruijnIndex ) -> Self

A convenient alternative to

`try_fold_with`

for use with infallible
folders. Do not override this method, to ensure coherence with
`try_fold_with`

.source§### impl<I: Interner> TypeVisitable<I> for QuantifierKind

### impl<I: Interner> TypeVisitable<I> for QuantifierKind

source§#### fn visit_with<B>(
&self,
_visitor: &mut dyn TypeVisitor<I, BreakTy = B>,
_outer_binder: DebruijnIndex
) -> ControlFlow<B>

#### fn visit_with<B>( &self, _visitor: &mut dyn TypeVisitor<I, BreakTy = B>, _outer_binder: DebruijnIndex ) -> ControlFlow<B>

Apply the given visitor

`visitor`

to `self`

; `binders`

is the
number of binders that are in scope when beginning the
visitor. Typically `binders`

starts as 0, but is adjusted when
we encounter `Binders<T>`

in the IR or other similar
constructs.source§### impl<I: Interner> Zip<I> for QuantifierKind

### impl<I: Interner> Zip<I> for QuantifierKind

### impl Copy for QuantifierKind

### impl Eq for QuantifierKind

### impl StructuralEq for QuantifierKind

### impl StructuralPartialEq for QuantifierKind

## 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§

source§### impl<T, I> Shift<I> for Twhere
T: TypeFoldable<I>,
I: Interner,

### impl<T, I> Shift<I> for Twhere T: TypeFoldable<I>, I: Interner,

source§#### fn shifted_in(self, interner: I) -> T

#### fn shifted_in(self, interner: I) -> T

Shifts this term in one level of binders.

source§#### fn shifted_in_from(self, interner: I, source_binder: DebruijnIndex) -> T

#### fn shifted_in_from(self, interner: I, source_binder: DebruijnIndex) -> T

Shifts a term valid at

`outer_binder`

so that it is
valid at the innermost binder. See `DebruijnIndex::shifted_in_from`

for a detailed explanation.source§#### fn shifted_out_to(
self,
interner: I,
target_binder: DebruijnIndex
) -> Result<T, NoSolution>

#### fn shifted_out_to( self, interner: I, target_binder: DebruijnIndex ) -> Result<T, NoSolution>

Shifts a term valid at the innermost binder so that it is
valid at

`outer_binder`

. See `DebruijnIndex::shifted_out_to`

for a detailed explanation.source§#### fn shifted_out(self, interner: I) -> Result<T, NoSolution>

#### fn shifted_out(self, interner: I) -> Result<T, NoSolution>

Shifts this term out one level of binders.

source§### impl<T, I> VisitExt<I> for Twhere
I: Interner,
T: TypeVisitable<I>,

### impl<T, I> VisitExt<I> for Twhere I: Interner, T: TypeVisitable<I>,

source§#### fn has_free_vars(&self, interner: I) -> bool

#### fn has_free_vars(&self, interner: I) -> bool

Check whether there are free (non-bound) variables.