Type Alias chalk_recursive::UCanonicalGoal

pub type UCanonicalGoal<I> = UCanonical<InEnvironment<Goal<I>>>;

Aliased Type

struct UCanonicalGoal<I> {
    pub canonical: Canonical<InEnvironment<Goal<I>>>,
    pub universes: usize,
}

Fields

canonical: Canonical<InEnvironment<Goal<I>>>

The wrapped Canonical.

universes: usize

The number of universes that have been collapsed.

Implementations

impl<T> UCanonical<T>

where T: HasInterner,

pub fn is_trivial_substitution( &self, interner: <T as HasInterner>::Interner, canonical_subst: &Canonical<AnswerSubst<<T as HasInterner>::Interner>>, ) -> bool

Checks whether the universe canonical value is a trivial substitution (e.g. an identity substitution).

pub fn trivial_substitution( &self, interner: <T as HasInterner>::Interner, ) -> Substitution<<T as HasInterner>::Interner>

Creates an identity substitution.

Trait Implementations

impl<T> Clone for UCanonical<T>

where T: Clone + HasInterner,

fn clone(&self) -> UCanonical<T>

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<T> Debug for UCanonical<T>

where T: Debug + HasInterner,

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl<T> Hash for UCanonical<T>

where T: Hash + HasInterner,

fn hash<__H>(&self, state: &mut __H)

where __H: Hasher,

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl<I> IsCoinductive<I> for UCanonical<InEnvironment<Goal<I>>>

where I: Interner,

fn is_coinductive(&self, db: &dyn RustIrDatabase<I>) -> bool

A goal G has coinductive semantics if proving G is allowed to assume G is true (very roughly speaking). In the case of chalk-ir, this is true for goals of the form T: AutoTrait, or if it is of the form WellFormed(T: Trait) where Trait is any trait. The latter is needed for dealing with WF requirements and cyclic traits, which generates cycles in the proof tree which must not be rejected but instead must be treated as a success.

impl<T> PartialEq for UCanonical<T>

where T: PartialEq + HasInterner,

fn eq(&self, other: &UCanonical<T>) -> bool

This method tests for self and other values to be equal, and is used by ==.

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

This method tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl<T> Eq for UCanonical<T>

where T: Eq + HasInterner,

impl<T> StructuralPartialEq for UCanonical<T>

where T: HasInterner,