def Lean.Meta.Grind.AC.get' : GoalM State

@[inline]

def Lean.Meta.Grind.AC.modify' (f : State → State) : GoalM Unit

def Lean.Meta.Grind.AC.checkMaxSteps : GoalM Bool

def Lean.Meta.Grind.AC.incSteps : GoalM Unit

structure Lean.Meta.Grind.AC.ACM.Context : Type

• opId : Nat

class Lean.Meta.Grind.AC.MonadGetStruct (m : Type → Type) : Type

• getStruct : m Struct

@[always_inline]

instance Lean.Meta.Grind.AC.instMonadGetStructOfMonadLift (m n : Type → Type) [MonadLift m n] [MonadGetStruct m] : MonadGetStruct n

@[reducible, inline]

abbrev Lean.Meta.Grind.AC.ACM (α : Type) : Type

@[reducible, inline]

abbrev Lean.Meta.Grind.AC.ACM.run {α : Type} (opId : Nat) (x : ACM α) : GoalM α

@[reducible, inline]

abbrev Lean.Meta.Grind.AC.getOpId : ACM Nat

def Lean.Meta.Grind.AC.ACM.getStruct : ACM Struct

instance Lean.Meta.Grind.AC.instMonadGetStructACM : MonadGetStruct ACM

def Lean.Meta.Grind.AC.modifyStruct (f : Struct → Struct) : ACM Unit

def Lean.Meta.Grind.AC.getOp : ACM Expr

def Lean.Meta.Grind.AC.getTermOpIds (e : Expr) : GoalM (List Nat)

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

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

def Lean.Meta.Grind.AC.getOpId? (op : Expr) : GoalM (Option Nat)

def Lean.Meta.Grind.AC.isOp? (e : Expr) : ACM (Option (Expr × Expr))

def Lean.Meta.Grind.AC.isCommutative : ACM Bool

def Lean.Meta.Grind.AC.hasNeutral : ACM Bool

def Lean.Meta.Grind.AC.isIdempotent : ACM Bool