Documentation

Mathlib.Tactic.Basic

Basic tactics and utilities for tactic writing #

This file defines some basic utilities for tactic writing, and also

Syntax for the variables command: this command is just a stub, and merely warns that it has been renamed to variable in Lean 4.

Equations
    Instances For

      The variables command: this is just a stub, and merely warns that it has been renamed to variable in Lean 4.

      Equations
        Instances For

          Given two arrays of FVarIds, one from an old local context and the other from a new local context, pushes FVarAliasInfos into the info tree for corresponding pairs of FVarIds. Recall that variables linked this way should be considered to be semantically identical.

          The effect of this is, for example, the unused variable linter will see that variables from the first array are used if corresponding variables in the second array are used.

          Equations
            Instances For

              The tactic introv allows the user to automatically introduce the variables of a theorem and explicitly name the non-dependent hypotheses. Any dependent hypotheses are assigned their default names.

              Examples:

              example : ∀ a b : Nat, a = b → b = a := by
                introv h,
                exact h.symm
              

              The state after introv h is

              a b : ℕ,
              h : a = b
              ⊢ b = a
              
              example : ∀ a b : Nat, a = b → ∀ c, b = c → a = c := by
                introv h₁ h₂,
                exact h₁.trans h₂
              

              The state after introv h₁ h₂ is

              a b : ℕ,
              h₁ : a = b,
              c : ℕ,
              h₂ : b = c
              ⊢ a = c
              
              Equations
                Instances For

                  Try calling assumption on all goals; succeeds if it closes at least one goal.

                  Equations
                    Instances For

                      This tactic clears all auxiliary declarations from the context.

                      Equations
                        Instances For