Documentation
Lean
.
Elab
.
Tactic
.
Conv
.
Simp
Search
Google site search
Lean
.
Elab
.
Tactic
.
Conv
.
Simp
source
Imports
Init
Lean.Elab.Tactic.Simp
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
.
evalSimpMatch
Lean
.
Elab
.
Tactic
.
Conv
.
evalDSimp
source
def
Lean
.
Elab
.
Tactic
.
Conv
.
applySimpResult
(result :
Lean.Meta.Simp.Result
)
:
Lean.Elab.Tactic.TacticM
Unit
Instances For
source
def
Lean
.
Elab
.
Tactic
.
Conv
.
evalSimp
:
Lean.Elab.Tactic.Tactic
Instances For
source
def
Lean
.
Elab
.
Tactic
.
Conv
.
evalSimpMatch
:
Lean.Elab.Tactic.Tactic
Instances For
source
def
Lean
.
Elab
.
Tactic
.
Conv
.
evalDSimp
:
Lean.Elab.Tactic.Tactic
Instances For