source
@[reducible, inline]
abbrev Lean.Meta.AC.ACExpr :
Type
Equations

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

Instances For

source
structure Lean.Meta.AC.PreContext :
Type

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

Instances For

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

- Lean.Meta.AC.instInhabitedPreContext = { default := Lean.Meta.AC.instInhabitedPreContext.default }

source
def Lean.Meta.AC.instInhabitedPreContext.default :
PreContext
Equations

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

Instances For

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

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

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

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

source
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.

Instances For

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

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

Instances For

source
inductive Lean.Meta.AC.PreExpr :
Type

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

Instances For

source
@[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

Instances For

source
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.

Instances For

source
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 #[] #[] #[]

Instances For

source
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.

Instances For

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

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

Instances For

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

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

Instances For

source
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

Instances For

source
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))

Instances For

source
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.

Instances For

source
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)

Instances For

source
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

Instances For

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

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

Instances For