@[reducible, inline]

abbrev Lean.Meta.AC.ACExpr : Type

Equations

• Lean.Meta.AC.ACExpr = Lean.Data.AC.Expr

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

Equations

• Lean.Meta.AC.instInhabitedPreContext = { default := { id := default, op := default, assoc := default, comm := default, idem := default } }

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.Meta.AC.bin op l r = (op.app l).app r

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

Equations

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

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

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 (l.op 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)

Equations

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

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)

Equations

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

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

Equations

• Lean.Meta.AC.buildNormProof.convert (l.op 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 Lean.MVarId

Equations

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

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

Equations

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

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

Equations

• Lean.Meta.AC.rewriteUnnormalizedRefl goal = do let newGoal ← Lean.Meta.AC.rewriteUnnormalized goal newGoal.refl

def Lean.Meta.AC.rewriteUnnormalizedNormalForm (goal : Lean.MVarId) : Lean.Elab.Tactic.TacticM Unit

Equations

• Lean.Meta.AC.rewriteUnnormalizedNormalForm goal = do let newGoal ← liftM (Lean.Meta.AC.rewriteUnnormalized goal) Lean.Elab.Tactic.replaceMainGoal [newGoal]

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

Equations

• Lean.Meta.AC.acRflTactic x = do let goal ← Lean.Elab.Tactic.getMainGoal goal.withContext (liftM (Lean.Meta.AC.rewriteUnnormalizedRefl goal))

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

Equations

• Lean.Meta.AC.acNfTactic x = do let goal ← Lean.Elab.Tactic.getMainGoal goal.withContext (Lean.Meta.AC.rewriteUnnormalizedNormalForm goal)