def Lean.Meta.Grind.proveEq? (lhs rhs : Expr) : GoalM (Option Expr)

Try to construct a proof that lhs = rhs using the information in the goal state. If lhs and rhs have not been internalized, this function will internalize then, process propagated equalities, and then check whether they are in the same equivalence class or not. The goal state is not modified by this function. This function mainly relies on congruence closure, and constraint propagation. It will not perform case analysis.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.proveHEq? (lhs rhs : Expr) : GoalM (Option Expr)

Similiar to proveEq?, but for heterogeneous equality.

Equations

• One or more equations did not get rendered due to their size.