Enum chalk_ir::QuantifierKind [−][src]
pub enum QuantifierKind { ForAll, Exists, }
Expand description
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]
impl Clone for QuantifierKind
[src]fn clone(&self) -> QuantifierKind
[src]
fn clone(&self) -> QuantifierKind
[src]Returns a copy of the value. Read more
fn clone_from(&mut self, source: &Self)
1.0.0[src]
fn clone_from(&mut self, source: &Self)
1.0.0[src]Performs copy-assignment from source
. Read more
impl Debug for QuantifierKind
[src]
impl Debug for QuantifierKind
[src]impl<I: Interner> Fold<I> for QuantifierKind
[src]
impl<I: Interner> Fold<I> for QuantifierKind
[src]type Result = Self
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>,
_outer_binder: DebruijnIndex
) -> Fallible<Self::Result> where
I: 'i,
[src]
fn fold_with<'i>(
self,
_folder: &mut dyn Folder<'i, I>,
_outer_binder: DebruijnIndex
) -> Fallible<Self::Result> where
I: 'i,
[src]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. Read more
impl Hash for QuantifierKind
[src]
impl Hash for QuantifierKind
[src]impl Ord for QuantifierKind
[src]
impl Ord for QuantifierKind
[src]impl PartialEq<QuantifierKind> for QuantifierKind
[src]
impl PartialEq<QuantifierKind> for QuantifierKind
[src]impl PartialOrd<QuantifierKind> for QuantifierKind
[src]
impl PartialOrd<QuantifierKind> for QuantifierKind
[src]fn partial_cmp(&self, other: &QuantifierKind) -> Option<Ordering>
[src]
fn partial_cmp(&self, other: &QuantifierKind) -> Option<Ordering>
[src]This method returns an ordering between self
and other
values if one exists. Read more
#[must_use]fn lt(&self, other: &Rhs) -> bool
1.0.0[src]
#[must_use]fn lt(&self, other: &Rhs) -> bool
1.0.0[src]This method tests less than (for self
and other
) and is used by the <
operator. Read more
#[must_use]fn le(&self, other: &Rhs) -> bool
1.0.0[src]
#[must_use]fn le(&self, other: &Rhs) -> bool
1.0.0[src]This method tests less than or equal to (for self
and other
) and is used by the <=
operator. Read more
impl<I: Interner> Visit<I> for QuantifierKind
[src]
impl<I: Interner> Visit<I> for QuantifierKind
[src]fn visit_with<'i, B>(
&self,
_visitor: &mut dyn Visitor<'i, I, BreakTy = B>,
_outer_binder: DebruijnIndex
) -> ControlFlow<B> where
I: 'i,
[src]
fn visit_with<'i, B>(
&self,
_visitor: &mut dyn Visitor<'i, I, BreakTy = B>,
_outer_binder: DebruijnIndex
) -> ControlFlow<B> where
I: 'i,
[src]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. Read more
impl<I: Interner> Zip<I> for QuantifierKind
[src]
impl<I: Interner> Zip<I> for QuantifierKind
[src]impl Copy for QuantifierKind
[src]
impl Eq for QuantifierKind
[src]
impl StructuralEq for QuantifierKind
[src]
impl StructuralPartialEq 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> BorrowMut<T> for T where
T: ?Sized,
[src]
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]pub fn borrow_mut(&mut self) -> &mut T
[src]
pub fn borrow_mut(&mut self) -> &mut T
[src]Mutably borrows from an owned value. Read more
impl<T> Cast for T
[src]
impl<T> Cast for T
[src]fn cast<U>(self, interner: &U::Interner) -> U where
Self: CastTo<U>,
U: HasInterner,
[src]
fn cast<U>(self, interner: &U::Interner) -> U where
Self: CastTo<U>,
U: HasInterner,
[src]Cast a value to type U
using CastTo
.
impl<T, I> Shift<I> for T where
T: Fold<I>,
I: Interner,
[src]
impl<T, I> Shift<I> for T where
T: Fold<I>,
I: Interner,
[src]pub fn shifted_in(Self, &I) -> <T as Fold<I>>::Result
[src]
pub fn shifted_in(Self, &I) -> <T as Fold<I>>::Result
[src]Shifts this term in one level of binders.
pub fn shifted_in_from(Self, &I, DebruijnIndex) -> <T as Fold<I>>::Result
[src]
pub fn shifted_in_from(Self, &I, DebruijnIndex) -> <T as Fold<I>>::Result
[src]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. Read more
pub fn shifted_out_to(
Self,
&I,
DebruijnIndex
) -> Result<<T as Fold<I>>::Result, NoSolution>
[src]
pub fn shifted_out_to(
Self,
&I,
DebruijnIndex
) -> Result<<T as Fold<I>>::Result, NoSolution>
[src]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. Read more
pub fn shifted_out(Self, &I) -> Result<<T as Fold<I>>::Result, NoSolution>
[src]
pub fn shifted_out(Self, &I) -> Result<<T as Fold<I>>::Result, NoSolution>
[src]Shifts this term out one level of binders.
impl<T> ToOwned for T where
T: Clone,
[src]
impl<T> ToOwned for T where
T: Clone,
[src]type Owned = T
type Owned = T
The resulting type after obtaining ownership.
pub fn to_owned(&self) -> T
[src]
pub fn to_owned(&self) -> T
[src]Creates owned data from borrowed data, usually by cloning. Read more
pub fn clone_into(&self, target: &mut T)
[src]
pub fn clone_into(&self, target: &mut T)
[src]🔬 This is a nightly-only experimental API. (toowned_clone_into
)
recently added
Uses borrowed data to replace owned data, usually by cloning. Read more