[][src]Trait chalk_solve::coinductive_goal::IsCoinductive

pub trait IsCoinductive<I: Interner> {
    fn is_coinductive(&self, db: &dyn RustIrDatabase<I>) -> bool;
}

Required methods

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.

Loading content...

Implementations on Foreign Types

impl<I: Interner> IsCoinductive<I> for Goal<I>[src]

impl<I: Interner> IsCoinductive<I> for UCanonical<InEnvironment<Goal<I>>>[src]

Loading content...

Implementors

Loading content...