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.

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

Instances For
    source
    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.

    Instances For
      source
      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.

      Instances For
        source
        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_let at ⊢ is a weaker form of intros that only introduces obvious lets.

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