# Documentation

Mathlib.Tactic.ExtractLets

# The extract_lets at tactic #

This module defines a tactic extract_lets ... at h that can be used to (in essence) do cases on a let expression.

def Lean.MVarId.extractLetsAt (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (names : ) :

Given a local hypothesis whose type is a let expression, then lift the let bindings to be a new local definition.

Instances For

Check that t is a let and then do what's necessary to lift it over the binding described by mk.

Instances For
def Lean.MVarId.extractLets (mvarId : Lean.MVarId) (names : ) :

A more limited version of Lean.MVarId.introN that ensures the goal is a nested let expression.

Instances For

The extract_lets at h tactic takes a local hypothesis of the form h : let x := v; b and introduces a new local definition x := v while changing h to be h : b. It can be thought of as being a cases tactic for let expressions. It can also be thought of as being like intros at h for let expressions.

For example, if h : let x := 1; x = x, then extract_lets x at h introduces x : Nat := 1 and changes h to h : x = x.

Just like intros, the extract_lets tactic either takes a list of names, in which case that specifies the number of let bindings that must be extracted, or it takes no names, in which case all the let bindings are extracted.

The tactic extract_let at ⊢ is a weaker form of intros that only introduces obvious lets.

Instances For
Instances For
def Mathlib.evalExtractLet.setupNames (ids? : Option (Lean.TSyntaxArray [ident, Lean.Parser.Term.hole])) (ty : Lean.Expr) :
Instances For
def Mathlib.evalExtractLet.doExtract (ids? : Option (Lean.TSyntaxArray [ident, Lean.Parser.Term.hole])) (loc : Lean.TSyntax `Lean.Parser.Tactic.location) :
Instances For