Trait chalk_solve::ext::GoalExt

pub trait GoalExt<I: Interner> {
    // Required methods
    fn into_peeled_goal(self, interner: I) -> UCanonical<InEnvironment<Goal<I>>>;
    fn into_closed_goal(self, interner: I) -> UCanonical<InEnvironment<Goal<I>>>;
}

Required Methods

fn into_peeled_goal(self, interner: I) -> UCanonical<InEnvironment<Goal<I>>>

fn into_closed_goal(self, interner: I) -> UCanonical<InEnvironment<Goal<I>>>

Implementations on Foreign Types

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

fn into_peeled_goal(self, interner: I) -> UCanonical<InEnvironment<Goal<I>>>

Returns a canonical goal in which the outermost exists<> and forall<> quantifiers (as well as implications) have been “peeled” and are converted into free universal or existential variables. Assumes that this goal is a “closed goal” which does not – at present – contain any variables. Useful for REPLs and tests but not much else.

fn into_closed_goal(self, interner: I) -> UCanonical<InEnvironment<Goal<I>>>

Given a goal with no free variables (a “closed” goal), creates a canonical form suitable for solving. This is a suitable choice if you don’t actually care about the values of any of the variables within; otherwise, you might want into_peeled_goal.

Panics

Will panic if this goal does in fact contain free variables.

Implementors