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.

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

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

      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.
      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_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.
        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_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.
          Instances For
            def Mathlib.evalExtractLets.setupNames (ids? : Option (Lean.TSyntaxArray [`ident, `Lean.Parser.Term.hole])) (ty : Lean.Expr) :
            Instances For
              def Mathlib.evalExtractLets.doExtract (ids? : Option (Lean.TSyntaxArray [`ident, `Lean.Parser.Term.hole])) (loc? : Option (Lean.TSyntax `Lean.Parser.Tactic.location)) :
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For