The lift_lets tactic

This module defines a tactic lift_lets that can be used to pull let bindings as far out of an expression as possible.

structure Lean.Expr.LiftLetsConfig : Type

Configuration for Lean.Expr.liftLets and the lift_lets tactic.

• proofs : Bool

  Whether to lift lets out of proofs. The default is not to.

• merge : Bool

  Whether to merge let bindings if they have the same type and value. This test is by syntactic equality, not definitional equality. The default is to merge.

def Lean.Expr.liftLets (e : Lean.Expr) (f : Array Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr) (config : optParam Lean.Expr.LiftLetsConfig { proofs := false, merge := true }) : Lean.MetaM Lean.Expr

Take all the lets in an expression and move them outwards as far as possible. All top-level lets are added to the local context, and then f is called with the list of local bindings (each an fvar) and the new expression.

Let bindings are merged if they have the same type and value.

Use e.liftLets mkLetFVars to get a defeq expression with all lets lifted as far as possible.

Equations

• e.liftLets f config = Lean.Expr.liftLetsAux config e #[] f

def Mathlib.Tactic.elabConfig : Lean.Syntax → Lean.Elab.Tactic.TacticM Lean.Expr.LiftLetsConfig

Equations

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

def Mathlib.Tactic.lift_lets : Lean.ParserDescr

Lift all the let bindings in the type of an expression as far out as possible.

When applied to the main goal, this gives one the ability to intro embedded let expressions. For example,

example : (let x := 1; x) = 1 := by
  lift_lets
  -- ⊢ let x := 1; x = 1
  intro x
  sorry

During the lifting process, let bindings are merged if they have the same type and value.

Equations

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