Documentation
Lean
.
Elab
.
Tactic
.
Conv
.
Simp
Search
return to top
source
Imports
Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.SimpTrace
Lean.Elab.Tactic.Split
Lean.Elab.Tactic.Conv.Basic
Imported by
Lean
.
Elab
.
Tactic
.
Conv
.
applySimpResult
Lean
.
Elab
.
Tactic
.
Conv
.
evalSimp
Lean
.
Elab
.
Tactic
.
Conv
.
evalSimpTrace
Lean
.
Elab
.
Tactic
.
Conv
.
evalSimpMatch
Lean
.
Elab
.
Tactic
.
Conv
.
evalDSimp
Lean
.
Elab
.
Tactic
.
Conv
.
evalDSimpTrace
source
def
Lean
.
Elab
.
Tactic
.
Conv
.
applySimpResult
(
result
:
Meta.Simp.Result
)
:
TacticM
Unit
Equations
Instances For
source
def
Lean
.
Elab
.
Tactic
.
Conv
.
evalSimp
:
Tactic
Equations
Instances For
source
def
Lean
.
Elab
.
Tactic
.
Conv
.
evalSimpTrace
:
Tactic
Equations
Instances For
source
def
Lean
.
Elab
.
Tactic
.
Conv
.
evalSimpMatch
:
Tactic
Equations
Instances For
source
def
Lean
.
Elab
.
Tactic
.
Conv
.
evalDSimp
:
Tactic
Equations
Instances For
source
def
Lean
.
Elab
.
Tactic
.
Conv
.
evalDSimpTrace
:
Tactic
Equations
Instances For