structure Lean.Meta.Grind.Homo.State : Type

Per-goal state for the [grind hom]/[grind hom_pred] solver extension.

• cache : Sym.Simp.Cache

  Persistent Sym.simp cache, reused across internalizations.

• internalized : PHashSet ExprPtr

  Terms already visited during internalization.

• initialized : Bool
• thms : Sym.Simp.Theorems

  [grind hom] rules, retrieved once per goal.

• preds : HomoPredTheorems

  [grind hom_pred] predicates, retrieved once per goal.

• sourceTypes : NameSet

  Head constants of the homomorphism source types, retrieved once per goal.

opaque Lean.Meta.Grind.Homo.homExt : SolverExtension State

def Lean.Meta.Grind.Homo.internalize (e : Expr) (_parent? : Option Expr) : GoalM Unit

Equations

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

def Lean.Meta.Grind.Homo.processNewEq (a b : Expr) : GoalM Unit

Equality hook: when the classes of a and b are merged and the [grind hom] set translates a = b, asserts the translated (and fully reduced) equality. This is the =-injection of the homomorphism: one fact per union, so a class with n elements produces n - 1 translated equalities; the transitive closure is handled by the target-domain E-graph, and asserting a = c after a = b and b = c is a no-op because no union takes place.

Equations

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

def Lean.Meta.Grind.Homo.processNewDiseq (a b : Expr) : GoalM Unit

Disequality hook: when a ≠ b is asserted and the [grind hom] set translates a = b, asserts the negation of the translated equality. Unlike equalities, disequalities are not propagated by congruence, and the target-domain solvers consume them directly (e.g. cutsat case splits on x ≠ 0). The translation is justified by the backward direction of the =-injection rule, i.e. the injectivity of the homomorphism.

Equations

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