Documentation
Lean
.
Elab
.
Tactic
.
Lets
Search
return to top
source
Imports
Lean.Elab.Tactic.Location
Lean.Meta.Tactic.Lets
Imported by
Lean
.
Elab
.
Tactic
.
linter
.
tactic
.
unusedName
Lean
.
Elab
.
Tactic
.
extractLetsAddVarInfo
Lean
.
Elab
.
Tactic
.
elabExtractLetsConfig
Lean
.
Elab
.
Tactic
.
elabLiftLetsConfig
Tactics to manipulate
let
expressions
#
source
opaque
Lean
.
Elab
.
Tactic
.
linter
.
tactic
.
unusedName
:
Lean.Option
Bool
extract_lets
#
source
def
Lean
.
Elab
.
Tactic
.
extractLetsAddVarInfo
(
ids
:
Array
Syntax
)
(
fvars
:
Array
FVarId
)
:
TacticM
Unit
Equations
Instances For
source
def
Lean
.
Elab
.
Tactic
.
elabExtractLetsConfig
:
Syntax
→
TacticM
Meta.ExtractLetsConfig
Equations
Instances For
lift_lets
#
source
def
Lean
.
Elab
.
Tactic
.
elabLiftLetsConfig
:
Syntax
→
TacticM
Meta.LiftLetsConfig
Equations
Instances For