[−][src]Trait chalk_engine::context::ResolventOps
Required methods
fn resolvent_clause(
&mut self,
interner: &I,
environment: &Environment<I>,
goal: &DomainGoal<I>,
subst: &Substitution<I>,
clause: &ProgramClause<I>
) -> Fallible<ExClause<I>>
&mut self,
interner: &I,
environment: &Environment<I>,
goal: &DomainGoal<I>,
subst: &Substitution<I>,
clause: &ProgramClause<I>
) -> Fallible<ExClause<I>>
Combines the goal
(instantiated within infer
) with the
given program clause to yield the start of a new strand (a
canonical ex-clause).
The bindings in infer
are unaffected by this operation.
fn apply_answer_subst(
&mut self,
interner: &I,
ex_clause: &mut ExClause<I>,
selected_goal: &InEnvironment<Goal<I>>,
answer_table_goal: &Canonical<InEnvironment<Goal<I>>>,
canonical_answer_subst: &Canonical<AnswerSubst<I>>
) -> Fallible<()>
&mut self,
interner: &I,
ex_clause: &mut ExClause<I>,
selected_goal: &InEnvironment<Goal<I>>,
answer_table_goal: &Canonical<InEnvironment<Goal<I>>>,
canonical_answer_subst: &Canonical<AnswerSubst<I>>
) -> Fallible<()>