@[reducible, inline]

abbrev Lean.Meta.AC.ACExpr : Type

Equations

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

Instances For

• Lean.Meta.AC.instEvalInformationPreContextACExpr

structure Lean.Meta.AC.PreContext : Type

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

Instances For

• Lean.Meta.AC.instEvalInformationPreContextACExpr
• Lean.Meta.AC.instInhabitedPreContext

instance Lean.Meta.AC.instInhabitedPreContext : Inhabited PreContext

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.Meta.AC.toACExpr.toPreExpr (op : Expr) : Expr → StateT ExprSet MetaM 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.ExprSet) => Std.HashSet.insert vars x✝ pure (Lean.Meta.AC.PreExpr.var x✝)

def Lean.Meta.AC.toACExpr.toACExpr (varMap : Expr → Nat) : PreExpr → 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 : 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.

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 : 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

Equations

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

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

Equations

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

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

Equations

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

def Lean.Meta.AC.buildNormProof.convert : ACExpr → 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 : PreContext) (vars : Array Expr) : ACExpr → 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 : Expr) : SimpM Simp.Step

Equations

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

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

Equations

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

def Lean.Meta.AC.rewriteUnnormalizedRefl (goal : MVarId) : 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 : 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 : MVarId) (fvarId : FVarId) : MetaM (Option MVarId)

Equations

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

def Lean.Meta.AC.acNfTargetTactic : 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 : FVarId) : 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 : Elab.Tactic.Tactic

Equations

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