Documentation

Mathlib.Tactic.Basic

source
def Mathlib.Tactic.variables :
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Mathlib.Tactic.elabVariables :
Lean.Elab.Command.CommandElab
Equations
  • One or more equations did not get rendered due to their size.
source
def Mathlib.Tactic.pushFVarAliasInfo {m : Type → Type} [Monad m] [Lean.Elab.MonadInfoTree m] (oldFVars : Array Lean.FVarId) (newFVars : Array Lean.FVarId) (newLCtx : Lean.LocalContext) :
m Unit

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
  • One or more equations did not get rendered due to their size.
source
def Mathlib.Tactic.introv :
Lean.ParserDescr

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
  • One or more equations did not get rendered due to their size.
source
def Mathlib.Tactic.evalIntrov :
Lean.Elab.Tactic.Tactic
Equations
  • One or more equations did not get rendered due to their size.
source
partial def Mathlib.Tactic.evalIntrov.introsDep :
Lean.Elab.Tactic.TacticM Unit
source
def Mathlib.Tactic.evalIntrov.intro1PStep :
Lean.Elab.Tactic.TacticM Unit
Equations
source
def Mathlib.Tactic.tacticAssumption' :
Lean.ParserDescr

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

Equations
source
def Mathlib.Tactic.tacticMatch_target_ :
Lean.ParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def Mathlib.Tactic.clearAuxDecl :
Lean.ParserDescr

This tactic clears all auxiliary declarations from the context.

Equations
source
def Lean.MVarId.clearValue (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) :
Lean.MetaM Lean.MVarId

Clears the value of the local definition fvarId. Ensures that the resulting goal state is still type correct. Throws an error if it is a local hypothesis without a value.

Equations
  • One or more equations did not get rendered due to their size.
source
def Mathlib.Tactic.clearValue :
Lean.ParserDescr

clear_value n₁ n₂ ... clears the bodies of the local definitions n₁, n₂ ..., changing them into regular hypotheses. A hypothesis n : α := t is changed to n : α.

The order of n₁ n₂ ... does not matter, and values will be cleared in reverse order of where they appear in the context.

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