@[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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

Equations

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

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

Equations

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

@[reducible, inline]

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

Equations

• Lean.Meta.Grind.AC.PropagateEqMap = Std.HashMap Lean.Grind.AC.Seq Lean.Meta.Grind.AC.EqData

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

Equations

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

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

Equations

• Lean.Meta.Grind.AC.check' = do let __do_lift ← Lean.Meta.Grind.AC.check pure (__do_lift != Lean.Meta.Grind.CheckResult.none)