@[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 : Lean.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 l r : Lean.Expr) : Lean.Expr

Equations

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

def Lean.Meta.AC.toACExpr (op l 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.abstractAtoms (preContext : Lean.Meta.AC.PreContext) (atoms : Array Lean.Expr) (k : Array (Lean.Expr × Option Lean.Expr) → Lean.MetaM Lean.Expr) : Lean.MetaM Lean.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.

Equations

• Lean.Meta.AC.abstractAtoms preContext atoms k = do let α ← Lean.Meta.inferType atoms[0]! let u ← Lean.Meta.getLevel α Lean.Meta.AC.abstractAtoms.go preContext atoms k α u 0 #[] #[] #[]

@[irreducible]

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

Equations

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

def Lean.Meta.AC.buildNormProof (preContext : Lean.Meta.AC.PreContext) (l 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 × Option Lean.Expr)) : Lean.MetaM 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.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.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.rewriteUnnormalizedRefl (goal : Lean.MVarId) : Lean.MetaM Unit

Equations

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

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.acNfHypMeta (goal : Lean.MVarId) (fvarId : Lean.FVarId) : Lean.MetaM (Option Lean.MVarId)

Equations

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

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

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

Equations

• Lean.Meta.AC.acNfTargetTactic = Lean.Elab.Tactic.liftMetaTactic1 fun (goal : Lean.MVarId) => do let a ← Lean.Meta.AC.rewriteUnnormalized goal pure (some a)

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

Implementation of the ac_nf tactic when operating on a hypothesis.

Equations

• Lean.Meta.AC.acNfHypTactic fvarId = Lean.Elab.Tactic.liftMetaTactic1 fun (goal : Lean.MVarId) => Lean.Meta.AC.acNfHypMeta goal fvarId

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

Equations

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