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))
Instances For
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))
Instances For
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.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Instances For
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.
Instances For
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.
Instances For
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.
Instances For
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.
Instances For
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.
Instances For
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.