Documentation
Lean
.
Elab
.
Tactic
.
Unfold
Search
return to top
source
Imports
Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.Location
Lean.Meta.Tactic.Unfold
Imported by
Lean
.
Elab
.
Tactic
.
unfoldLocalDecl
Lean
.
Elab
.
Tactic
.
unfoldTarget
Lean
.
Elab
.
Tactic
.
zetaDeltaLocalDecl
Lean
.
Elab
.
Tactic
.
zetaDeltaTarget
Lean
.
Elab
.
Tactic
.
evalUnfold
Lean
.
Elab
.
Tactic
.
evalUnfold
.
go
source
def
Lean
.
Elab
.
Tactic
.
unfoldLocalDecl
(
declName
:
Name
)
(
fvarId
:
FVarId
)
:
TacticM
Unit
Equations
Instances For
source
def
Lean
.
Elab
.
Tactic
.
unfoldTarget
(
declName
:
Name
)
:
TacticM
Unit
Equations
Instances For
source
def
Lean
.
Elab
.
Tactic
.
zetaDeltaLocalDecl
(
declFVarId
fvarId
:
FVarId
)
:
TacticM
Unit
Equations
Instances For
source
def
Lean
.
Elab
.
Tactic
.
zetaDeltaTarget
(
declFVarId
:
FVarId
)
:
TacticM
Unit
Equations
Instances For
source
def
Lean
.
Elab
.
Tactic
.
evalUnfold
:
Tactic
"unfold " ident+ (location)?
Equations
Instances For
source
def
Lean
.
Elab
.
Tactic
.
evalUnfold
.
go
(
declNameId
:
Syntax
)
(
loc
:
Location
)
:
TacticM
Unit
Equations
Instances For