Skip to main content

check_goal

logicaffeine_kernel::simp

Function check_goal 

Source 
pub fn check_goal(goal: &Term) -> bool
Expand description

Check if a goal is provable by simplification.

This is the main entry point for the simp tactic. It extracts hypothesis equalities as rewrites, simplifies both sides of the conclusion equality, and checks for syntactic equality.

§Supported Goals

  • Bare equalities: Eq a b where a simplifies to b
  • Implications: (Eq x 0) -> (Eq (add x 1) 1) using hypothesis as rewrite
  • Nested implications with multiple hypothesis rewrites

§Returns

true if the simplified LHS equals the simplified RHS, false otherwise.