Skip to main content

decompose_goal

logicaffeine_kernel::cc

Function decompose_goal 

Source 
pub fn decompose_goal(goal: &Term) -> (Vec<(Term, Term)>, Term)
Expand description

Decompose a goal into hypotheses and conclusion.

Peels off nested implications to extract equality hypotheses. For example, (h1 -> h2 -> conclusion) becomes ([h1, h2], conclusion).

ยงReturns

A tuple of:

  • Vector of equality hypothesis pairs (LHS, RHS)
  • The final conclusion term

Only equalities in hypothesis position are extracted; other hypotheses are ignored.