Documentation
Lean
.
Elab
.
Tactic
.
Simproc
Search
return to top
source
Imports
Init.Simproc
Lean.ReservedNameAction
Lean.Elab.Binders
Lean.Elab.Command
Lean.Elab.SyntheticMVars
Lean.Elab.Term
Lean.Meta.Tactic.Simp.Simproc
Imported by
Lean
.
Elab
.
elabSimprocPattern
Lean
.
Elab
.
elabSimprocKeys
Lean
.
Elab
.
checkSimprocType
Lean
.
Elab
.
Command
.
elabSimprocPattern
Lean
.
Elab
.
Command
.
elabSimprocPatternBuiltin
source
def
Lean
.
Elab
.
elabSimprocPattern
(
stx
:
Syntax
)
:
MetaM
Expr
Equations
Instances For
source
def
Lean
.
Elab
.
elabSimprocKeys
(
stx
:
Syntax
)
:
MetaM
(
Array
Meta.SimpTheoremKey
)
Equations
Instances For
source
def
Lean
.
Elab
.
checkSimprocType
(
declName
:
Name
)
:
CoreM
Bool
Equations
Instances For
source
def
Lean
.
Elab
.
Command
.
elabSimprocPattern
:
CommandElab
Equations
Instances For
source
def
Lean
.
Elab
.
Command
.
elabSimprocPatternBuiltin
:
CommandElab
Equations
Instances For