# 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

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Elab.Tactic.elabExtractLetsConfig :
Syntax → TacticM Meta.ExtractLetsConfig
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Elab.Tactic.evalExtractLets :
Tactic
Equations

- One or more equations did not get rendered due to their size.

Instances For

### `lift_lets` #

source
def Lean.Elab.Tactic.elabLiftLetsConfig :
Syntax → TacticM Meta.LiftLetsConfig
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Elab.Tactic.evalLiftLets :
Tactic
Equations

- One or more equations did not get rendered due to their size.

Instances For

### `let_to_have` #

source
def Lean.Elab.Tactic.evalLetToHave :
Tactic
Equations

- One or more equations did not get rendered due to their size.

Instances For