Documentation

Lean.Elab.Tactic.Rewrite

source
def Lean.Elab.Tactic.rewriteTarget (stx : Lean.Syntax) (symm : Bool) (config : Lean.Meta.Rewrite.Config) :
Lean.Elab.Tactic.TacticM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.rewriteLocalDecl (stx : Lean.Syntax) (symm : Bool) (fvarId : Lean.FVarId) (config : Lean.Meta.Rewrite.Config) :
Lean.Elab.Tactic.TacticM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.withRWRulesSeq (token : Lean.Syntax) (rwRulesSeqStx : Lean.Syntax) (x : Bool → Lean.Syntax → Lean.Elab.Tactic.TacticM Unit) :
Lean.Elab.Tactic.TacticM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.withRWRulesSeq.go (x : Bool → Lean.Syntax → Lean.Elab.Tactic.TacticM Unit) (symm : Bool) (id : Lean.Syntax) (declName : Lean.Name) :
List Lean.Name → Lean.Elab.Tactic.TacticM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.elabRewriteConfig:
Lean.Syntax → Lean.Elab.TermElabM Lean.Meta.Rewrite.Config
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Tactic.evalRewriteSeq:
Lean.Elab.Tactic.Tactic
Equations
  • One or more equations did not get rendered due to their size.