@[inline, reducible]

abbrev Lean.Meta.AC.ACExpr : Type

structure Lean.Meta.AC.PreContext : Type

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

instance Lean.Meta.AC.instInhabitedPreContext : Inhabited Lean.Meta.AC.PreContext

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

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

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

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

inductive Lean.Meta.AC.PreExpr : Type

• op: Lean.Meta.AC.PreExpr → Lean.Meta.AC.PreExpr → Lean.Meta.AC.PreExpr
• var: Lean.Expr → Lean.Meta.AC.PreExpr

@[match_pattern]

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

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

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.AC.toACExpr.toPreExpr op x = do modify fun vars => Lean.HashSet.insert vars x pure (Lean.Meta.AC.PreExpr.var x)

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

Equations

• Lean.Meta.AC.toACExpr.toACExpr varMap (Lean.Meta.AC.PreExpr.op l r) = Lean.Data.AC.Expr.op (Lean.Meta.AC.toACExpr.toACExpr varMap l) (Lean.Meta.AC.toACExpr.toACExpr varMap r)
• Lean.Meta.AC.toACExpr.toACExpr varMap (Lean.Meta.AC.PreExpr.var x_1) = Lean.Data.AC.Expr.var (varMap x_1)

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

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

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

Equations

• Lean.Meta.AC.buildNormProof.convert (Lean.Data.AC.Expr.op l r) = Lean.mkApp2 (Lean.mkConst `Lean.Data.AC.Expr.op) (Lean.Meta.AC.buildNormProof.convert l) (Lean.Meta.AC.buildNormProof.convert r)
• Lean.Meta.AC.buildNormProof.convert (Lean.Data.AC.Expr.var x_1) = Lean.mkApp (Lean.mkConst `Lean.Data.AC.Expr.var) (Lean.mkNatLit x_1)

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

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.AC.buildNormProof.convertTarget preContext vars (Lean.Data.AC.Expr.var x_1) = vars[x_1]!

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

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

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