Trait chalk_solve::coinductive_goal::IsCoinductive

pub trait IsCoinductive<I: Interner> {
    // Required method
    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.

Implementations on Foreign Types

impl<I: Interner> IsCoinductive<I> for Goal<I>

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

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

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

Implementors