Documentation

Lean.Meta.Tactic.AC.Main

source
@[inline]
abbrev Lean.Meta.AC.ACExpr:
Type
Equations
source
structure Lean.Meta.AC.PreContext:
Type
source
instance Lean.Meta.AC.instInhabitedPreContext:
Inhabited Lean.Meta.AC.PreContext
Equations
source
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.
source
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.
source
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.
source
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.
source
inductive Lean.Meta.AC.PreExpr:
Type
source
@[matchPattern]
def Lean.Meta.AC.bin {x₁ : Lean.Expr.Data} {x₂ : Lean.Expr.Data} (op : Lean.Expr) (l : Lean.Expr) (r : Lean.Expr) :
Lean.Expr
Equations
source
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.
source
def Lean.Meta.AC.toACExpr.toPreExpr (op : Lean.Expr) :
Lean.Expr → StateT Lean.ExprSet Lean.MetaM Lean.Meta.AC.PreExpr
source
def Lean.Meta.AC.toACExpr.toACExpr (varMap : Lean.Expr → Nat) :
Lean.Meta.AC.PreExpr → Lean.Meta.AC.ACExpr
Equations
source
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.
source
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.
source
def Lean.Meta.AC.buildNormProof.convert:
Lean.Meta.AC.ACExpr → Lean.Expr
Equations
source
def Lean.Meta.AC.buildNormProof.convertTarget (preContext : Lean.Meta.AC.PreContext) (vars : Array Lean.Expr) :
Lean.Meta.AC.ACExpr → Lean.Expr
Equations
source
def Lean.Meta.AC.rewriteUnnormalized (mvarId : Lean.MVarId) :
Lean.MetaM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
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.
source
def Lean.Meta.AC.ac_refl_tactic:
Lean.Elab.Tactic.Tactic
Equations