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

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

Instances For

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

Instances For

source
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))

Instances For

source
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 }

Instances For

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

- opId : Nat

Instances For

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

- getStruct : m Struct

Instances

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

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

Instances For

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

Instances For

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

Instances For

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

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

Instances For

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

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

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

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

Instances For

source
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

Instances For

source
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 [])

Instances For

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

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

Instances For

source
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.

Instances For

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

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

Instances For

source
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.

Instances For

source
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

Instances For

source
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

Instances For

source
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

Instances For