Documentation

Mathlib.Tactic.LiftLets

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.

  • 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.

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

Instances For

    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.

    Instances For

      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.

      Instances For