@[reducible, inline]

abbrev Lean.Meta.AC.ACExpr : Type

structure Lean.Meta.AC.PreContext : Type

• id : Nat
• op : Expr
• assoc : Expr
• comm : Option Expr
• idem : Option Expr

instance Lean.Meta.AC.instInhabitedPreContext : Inhabited PreContext

instance Lean.Meta.AC.instContextInformationProdPreContextArrayBool : Data.AC.ContextInformation (PreContext × Array Bool)

instance Lean.Meta.AC.instEvalInformationPreContextACExpr : Data.AC.EvalInformation PreContext ACExpr

def Lean.Meta.AC.getInstance (cls : Name) (exprs : Array Expr) : MetaM (Option Expr)

def Lean.Meta.AC.preContext (expr : Expr) : MetaM (Option PreContext)

inductive Lean.Meta.AC.PreExpr : Type

• op (lhs rhs : PreExpr) : PreExpr
• var (e : Expr) : PreExpr

@[match_pattern]

def Lean.Meta.AC.bin (op l r : Expr) : Expr

def Lean.Meta.AC.toACExpr (op l r : Expr) : MetaM (Array Expr × ACExpr)

def Lean.Meta.AC.toACExpr.toPreExpr (op : Expr) : Expr → StateT ExprSet MetaM PreExpr

def Lean.Meta.AC.toACExpr.toACExpr (varMap : Expr → Nat) : PreExpr → ACExpr

def Lean.Meta.AC.abstractAtoms (preContext : PreContext) (atoms : Array Expr) (k : Array (Expr × Option Expr) → MetaM Expr) : MetaM Expr

In order to prevent the kernel trying to reduce the atoms of the expression, we abstract the proof over them. But ac_rfl proofs are not completely abstract in the value of the atoms – it recognizes neutral elements. So we have to abstract over these proofs as well.

@[irreducible]

def Lean.Meta.AC.abstractAtoms.go (preContext : PreContext) (atoms : Array Expr) (k : Array (Expr × Option Expr) → MetaM Expr) (α : Expr) (u : Level) (i : Nat) (acc : Array (Expr × Option Expr)) (vars args : Array Expr) : MetaM Expr

def Lean.Meta.AC.buildNormProof (preContext : PreContext) (l r : Expr) : MetaM (Expr × Expr)

def Lean.Meta.AC.buildNormProof.mkContext (preContext : PreContext) (α : Expr) (u : Level) (vars : Array (Expr × Option Expr)) : MetaM Expr

def Lean.Meta.AC.buildNormProof.convert : ACExpr → Expr

def Lean.Meta.AC.buildNormProof.convertTarget (preContext : PreContext) (vars : Array Expr) : ACExpr → Expr

def Lean.Meta.AC.post (e : Expr) : SimpM Simp.Step

def Lean.Meta.AC.rewriteUnnormalized (mvarId : MVarId) : MetaM MVarId

def Lean.Meta.AC.rewriteUnnormalizedRefl (goal : MVarId) : MetaM Unit

def Lean.Meta.AC.acRflTactic : Elab.Tactic.Tactic

def Lean.Meta.AC.acNfHypMeta (goal : MVarId) (fvarId : FVarId) : MetaM (Option MVarId)

def Lean.Meta.AC.acNfTargetTactic : Elab.Tactic.TacticM Unit

Implementation of the ac_nf tactic when operating on the main goal.

def Lean.Meta.AC.acNfHypTactic (fvarId : FVarId) : Elab.Tactic.TacticM Unit

Implementation of the ac_nf tactic when operating on a hypothesis.

def Lean.Meta.AC.evalNf0 : Elab.Tactic.Tactic