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

Equations

• Lean.Meta.Grind.AC.get' = Lean.Meta.Grind.AC.acExt.getState

@[inline]

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

Equations

• Lean.Meta.Grind.AC.modify' f = Lean.Meta.Grind.AC.acExt.modifyState f

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

Equations

• Lean.Meta.Grind.AC.checkMaxSteps = do let __do_lift ← Lean.Meta.Grind.AC.get' let __do_lift_1 ← liftM Lean.Meta.Grind.getConfig pure (decide (__do_lift.steps ≥ __do_lift_1.acSteps))

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

Equations

• Lean.Meta.Grind.AC.incSteps = Lean.Meta.Grind.AC.modify' fun (s : Lean.Meta.Grind.AC.State) => { structs := s.structs, opIdOf := s.opIdOf, exprToOpIds := s.exprToOpIds, steps := s.steps + 1 }

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

Equations

• Lean.Meta.Grind.AC.instMonadGetStructOfMonadLift m n = { getStruct := liftM Lean.Meta.Grind.AC.getStruct }

@[reducible, inline]

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

Equations

• Lean.Meta.Grind.AC.ACM = ReaderT Lean.Meta.Grind.AC.ACM.Context Lean.Meta.Grind.GoalM

@[reducible, inline]

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

Equations

• Lean.Meta.Grind.AC.ACM.run opId x = x { opId := opId }

@[reducible, inline]

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

Equations

• Lean.Meta.Grind.AC.getOpId = do let __do_lift ← read pure __do_lift.opId

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

Equations

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

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

Equations

• Lean.Meta.Grind.AC.instMonadGetStructACM = { getStruct := Lean.Meta.Grind.AC.ACM.getStruct }

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

Equations

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

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

Equations

• Lean.Meta.Grind.AC.getOp = do let __do_lift ← Lean.Meta.Grind.AC.getStruct pure __do_lift.op

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

Equations

• Lean.Meta.Grind.AC.getTermOpIds e = do let __do_lift ← Lean.Meta.Grind.AC.get' pure ((Lean.PersistentHashMap.find? __do_lift.exprToOpIds { expr := e }).getD [])

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.Meta.Grind.AC.isCommutative = do let __do_lift ← Lean.Meta.Grind.AC.getStruct pure __do_lift.commInst?.isSome

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

Equations

• Lean.Meta.Grind.AC.hasNeutral = do let __do_lift ← Lean.Meta.Grind.AC.getStruct pure __do_lift.neutralInst?.isSome

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

Equations

• Lean.Meta.Grind.AC.isIdempotent = do let __do_lift ← Lean.Meta.Grind.AC.getStruct pure __do_lift.idempotentInst?.isSome