def Lean.termEval_prec_ : ParserDescr

Equations

• Lean.termEval_prec_ = Lean.ParserDescr.node `Lean.termEval_prec_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "eval_prec ") (Lean.ParserDescr.cat `prec 1024))

def Lean.termEval_prio_ : ParserDescr

Equations

• Lean.termEval_prio_ = Lean.ParserDescr.node `Lean.termEval_prio_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "eval_prio ") (Lean.ParserDescr.cat `prio 1024))

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

Equations

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

def Lean.Parser.Tactic.simpAllKind : ParserDescr

Equations

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

def Lean.Parser.Tactic.dsimpKind : ParserDescr

Equations

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

def Lean.Parser.Tactic.declareSimpLikeTactic : ParserDescr

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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