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 : Array Lean.Name) : Lean.MetaM (Array Lean.FVarId × Lean.MVarId)

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

Equations

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

def Lean.MVarId.extractLetsAt.process (mvarId : Lean.MVarId) (t : Lean.Expr) (mk : Lean.Expr → Lean.Expr) : Lean.MetaM Lean.MVarId

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

Equations

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

def Lean.MVarId.extractLets (mvarId : Lean.MVarId) (names : Array Lean.Name) : Lean.MetaM (Array Lean.FVarId × Lean.MVarId)

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

Equations

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

def Mathlib.extractLets : Lean.ParserDescr

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_lets (without at) or extract_lets at h ⊢ acts as a weaker form of intros on the goal that only introduces obvious lets.

Equations

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

def Mathlib.evalExtractLets : Lean.Elab.Tactic.Tactic

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_lets (without at) or extract_lets at h ⊢ acts as a weaker form of intros on the goal that only introduces obvious lets.

Equations

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

def Mathlib.evalExtractLets.setupNames (ids? : Option (Lean.TSyntaxArray [`ident, `Lean.Parser.Term.hole])) (ty : Lean.Expr) : Lean.MetaM (Array Lean.Name)

Equations

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

def Mathlib.evalExtractLets.doExtract (ids? : Option (Lean.TSyntaxArray [`ident, `Lean.Parser.Term.hole])) (loc? : Option (Lean.TSyntax `Lean.Parser.Tactic.location)) : Lean.Elab.Tactic.TacticM Unit

Equations

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