def Lean.termEval_prec_ : ParserDescr

def Lean.termEval_prio_ : ParserDescr

def Lean.Parser.Tactic.tacticErw___ : ParserDescr

erw [rules] is a shorthand for rw (transparency := .default) [rules]. This does rewriting up to unfolding of regular definitions (by comparison to regular rw which only unfolds @[reducible] definitions).

def Lean.Parser.Tactic.simpAllKind : ParserDescr

def Lean.Parser.Tactic.dsimpKind : ParserDescr

def Lean.Parser.Tactic.declareSimpLikeTactic : ParserDescr

def Lean.Parser.Tactic.simpAutoUnfold : ParserDescr

simp! is shorthand for simp with autoUnfold := true. This will unfold applications of functions defined by pattern matching, when one of the patterns applies. This can be used to partially evaluate many definitions.

def Lean.Parser.Tactic.simpArith : ParserDescr

simp_arith has been deprecated. It was a shorthand for simp +arith +decide. Note that +decide is not needed for reducing arithmetic terms since simprocs have been added to Lean.

def Lean.Parser.Tactic.simpArithBang : ParserDescr

simp_arith! has been deprecated. It was a shorthand for simp! +arith +decide. Note that +decide is not needed for reducing arithmetic terms since simprocs have been added to Lean.

def Lean.Parser.Tactic.simpAllAutoUnfold : ParserDescr

simp_all! is shorthand for simp_all with autoUnfold := true. This will unfold applications of functions defined by pattern matching, when one of the patterns applies. This can be used to partially evaluate many definitions.

def Lean.Parser.Tactic.simpAllArith : ParserDescr

simp_all_arith has been deprecated. It was a shorthand for simp_all +arith +decide. Note that +decide is not needed for reducing arithmetic terms since simprocs have been added to Lean.

def Lean.Parser.Tactic.simpAllArithBang : ParserDescr

simp_all_arith! has been deprecated. It was a shorthand for simp_all! +arith +decide. Note that +decide is not needed for reducing arithmetic terms since simprocs have been added to Lean.

def Lean.Parser.Tactic.dsimpAutoUnfold : ParserDescr

dsimp! is shorthand for dsimp with autoUnfold := true. This will unfold applications of functions defined by pattern matching, when one of the patterns applies. This can be used to partially evaluate many definitions.