Documentation
Lean
.
Elab
.
Tactic
.
Delta
Search
Google site search
Lean
.
Elab
.
Tactic
.
Delta
source
Imports
Init
Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.Location
Lean.Meta.Tactic.Delta
Imported by
Lean
.
Elab
.
Tactic
.
deltaLocalDecl
Lean
.
Elab
.
Tactic
.
deltaTarget
Lean
.
Elab
.
Tactic
.
evalDelta
source
def
Lean
.
Elab
.
Tactic
.
deltaLocalDecl
(declNames :
Array
Lake.Name
)
(fvarId :
Lean.FVarId
)
:
Lean.Elab.Tactic.TacticM
Unit
Instances For
source
def
Lean
.
Elab
.
Tactic
.
deltaTarget
(declNames :
Array
Lake.Name
)
:
Lean.Elab.Tactic.TacticM
Unit
Instances For
source
def
Lean
.
Elab
.
Tactic
.
evalDelta
:
Lean.Elab.Tactic.Tactic
"delta " ident+ (location)?
Instances For