@[specialize #[]]

def Lean.Meta.Grind.AC.withExprs (a b : Expr) (k : ACM Unit) : GoalM Unit

For each structure s s.t. a and b are elements of, execute k

def Lean.Meta.Grind.AC.asACExpr (e : Expr) : ACM Grind.AC.Expr

def Lean.Meta.Grind.AC.norm (e : Grind.AC.Expr) : ACM Grind.AC.Seq

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

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

def Lean.Meta.Grind.AC.EqCnstr.simplifyRHS (c : EqCnstr) : ACM EqCnstr

Simplifies the right-hand-side of the given equation.

structure Lean.Meta.Grind.AC.EqData : Type

Data for equality propagation. We maintain a mapping from sequences to EqData

• e : Expr
• r : Grind.AC.Expr
• c : EqCnstr

def Lean.Meta.Grind.AC.mkEqData (e : Expr) (r : Grind.AC.Expr) : ACM EqData

@[reducible, inline]

abbrev Lean.Meta.Grind.AC.PropagateEqMap : Type

def Lean.Meta.Grind.AC.check : GoalM CheckResult

def Lean.Meta.Grind.AC.check' : GoalM Bool