Documentation

Lean.Elab.Tactic.Rewrite

Equations
  • One or more equations did not get rendered due to their size.
def Lean.Elab.Tactic.rewriteLocalDecl (stx : Syntax) (symm : Bool) (fvarId : FVarId) (config : Meta.Rewrite.Config := { transparency := Meta.TransparencyMode.reducible, offsetCnstrs := true, occs := Meta.Occurrences.all, newGoals := Meta.ApplyNewGoals.nonDependentFirst }) :
Equations
  • One or more equations did not get rendered due to their size.
def Lean.Elab.Tactic.withRWRulesSeq (token rwRulesSeqStx : Syntax) (x : BoolSyntaxTacticM Unit) :
Equations
  • One or more equations did not get rendered due to their size.
def Lean.Elab.Tactic.withRWRulesSeq.go (x : BoolSyntaxTacticM Unit) (symm : Bool) (id : Syntax) (declName : Name) (hint : MessageData) :
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.