Generally useful tactics.

def Lean.toModifiers (nm : Lean.Name) (newDoc : optParam (Option String) none) : Lean.CoreM Lean.Elab.Modifiers

Return the modifiers of declaration nm with (optional) docstring newDoc. Currently, recursive or partial definitions are not supported, and no attributes are provided.

Equations

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

def Lean.toPreDefinition (nm : Lean.Name) (newNm : Lean.Name) (newType : Lean.Expr) (newValue : Lean.Expr) (newDoc : optParam (Option String) none) : Lean.CoreM Lean.Elab.PreDefinition

Make a PreDefinition taking some metadata from declaration nm. You can provide a new type, value and (optional) docstring, but the remaining information is taken from nm. Currently only implemented for definitions and theorems. Also see docstring of toModifiers

Equations

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

def Lean.setProtected {m : Type → Type} [Lean.MonadEnv m] (nm : Lean.Name) : m Unit

Make nm protected.

Equations

• Lean.setProtected nm = Lean.modifyEnv fun (x : Lean.Environment) => Lean.addProtected x nm

def Lean.MVarId.introsWithBinderIdents (g : Lean.MVarId) (ids : List (Lean.TSyntax `Lean.binderIdent)) : Lean.MetaM (List (Lean.TSyntax `Lean.binderIdent) × Array Lean.FVarId × Lean.MVarId)

Introduce variables, giving them names from a specified list.

Equations

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

def Mathlib.Tactic.withArgs : Lean.ParserDescr

Equations

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

def Mathlib.Tactic.usingArg : Lean.ParserDescr

Equations

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

def Mathlib.Tactic.getSimpArgs : Lean.Syntax → Lean.Elab.Tactic.TacticM (Array Lean.Syntax)

Extract the arguments from a simpArgs syntax as an array of syntaxes

Equations

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

def Mathlib.Tactic.getDSimpArgs : Lean.Syntax → Lean.Elab.Tactic.TacticM (Array Lean.Syntax)

Extract the arguments from a dsimpArgs syntax as an array of syntaxes

Equations

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

def Mathlib.Tactic.getWithArgs : Lean.Syntax → Lean.Elab.Tactic.TacticM (Array Lean.Syntax)

Extract the arguments from a withArgs syntax as an array of syntaxes

Equations

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

def Mathlib.Tactic.getUsingArg : Lean.Syntax → Lean.Elab.Tactic.TacticM Lean.Syntax

Extract the argument from a usingArg syntax as a syntax term

Equations

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

def Mathlib.Tactic.tacticRepeat1_ : Lean.ParserDescr

repeat1 tac applies tac to main goal at least once. If the application succeeds, the tactic is applied recursively to the generated subgoals until it eventually fails.

Equations

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

def Lean.Elab.Tactic.filterOutImplementationDetails (lctx : Lean.LocalContext) (fvarIds : Array Lean.FVarId) : Array Lean.FVarId

Given a local context and an array of FVarIds assumed to be in that local context, remove all implementation details.

Equations

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

def Lean.Elab.Tactic.getFVarIdAt (goal : Lean.MVarId) (id : Lean.Syntax) : Lean.Elab.Tactic.TacticM Lean.FVarId

Elaborate syntax for an FVarId in the local context of the given goal.

Equations

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

def Lean.Elab.Tactic.getFVarIdsAt (goal : Lean.MVarId) (ids : optParam (Option (Array Lean.Syntax)) none) (includeImplementationDetails : optParam Bool false) : Lean.Elab.Tactic.TacticM (Array Lean.FVarId)

Get the array of FVarIds in the local context of the given goal.

If ids is specified, elaborate them in the local context of the given goal to obtain the array of FVarIds.

If includeImplementationDetails is false (the default), we filter out implementation details (implDecls and auxDecls) from the resulting list of FVarIds.

Equations

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

def Lean.Elab.Tactic.allGoals (tac : Lean.Elab.Tactic.TacticM Unit) : Lean.Elab.Tactic.TacticM Unit

Run a tactic on all goals, and always succeeds.

(This is parallel to Lean.Elab.Tactic.evalAllGoals in core, which takes a Syntax rather than TacticM Unit. This function could be moved to core and evalAllGoals refactored to use it.)

Equations

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

def Lean.Elab.Tactic.andThenOnSubgoals (tac1 : Lean.Elab.Tactic.TacticM Unit) (tac2 : Lean.Elab.Tactic.TacticM Unit) : Lean.Elab.Tactic.TacticM Unit

Simulates the <;> tactic combinator. First runs tac1 and then runs tac2 on all newly-generated subgoals.

Equations

• Lean.Elab.Tactic.andThenOnSubgoals tac1 tac2 = Lean.Elab.Tactic.focus do tac1 Lean.Elab.Tactic.allGoals tac2

def Lean.Elab.Tactic.iterateAtMost {m : Type → Type u_1} [Monad m] [MonadExcept Lean.Exception m] : Nat → m Unit → m Unit

Repeats a tactic at most n times, stopping sooner if the tactic fails. Always succeeds.

Equations

• Lean.Elab.Tactic.iterateAtMost 0 x = pure ()
• Lean.Elab.Tactic.iterateAtMost (Nat.succ n) x = tryCatch (do x Lean.Elab.Tactic.iterateAtMost n x) fun (x : Lean.Exception) => pure ()

def Lean.Elab.Tactic.iterateExactly' {m : Type → Type u_1} [Monad m] : Nat → m Unit → m Unit

iterateExactly' n t executes t n times. If any iteration fails, the whole tactic fails.

Equations

• Lean.Elab.Tactic.iterateExactly' 0 x = pure ()
• Lean.Elab.Tactic.iterateExactly' (Nat.succ n) x = SeqRight.seqRight x fun (x_1 : Unit) => Lean.Elab.Tactic.iterateExactly' n x

def Lean.Elab.Tactic.iterateRange {m : Type → Type u_1} [Monad m] [MonadExcept Lean.Exception m] : Nat → Nat → m Unit → m Unit

iterateRange m n t: Repeat the given tactic at least m times and at most n times or until t fails. Fails if t does not run at least m times.

Equations

• Lean.Elab.Tactic.iterateRange 0 0 x = pure ()
• Lean.Elab.Tactic.iterateRange 0 x✝ x = Lean.Elab.Tactic.iterateAtMost x✝ x
• Lean.Elab.Tactic.iterateRange (Nat.succ a) x✝ x = do x Lean.Elab.Tactic.iterateRange a (x✝ - 1) x

partial def Lean.Elab.Tactic.iterateUntilFailure {m : Type → Type u_1} [Monad m] [MonadExcept Lean.Exception m] (tac : m Unit) : m Unit

Repeats a tactic until it fails. Always succeeds.

partial def Lean.Elab.Tactic.iterateUntilFailureWithResults {m : Type → Type u_1} [Monad m] [MonadExcept Lean.Exception m] {α : Type} (tac : m α) : m (List α)

iterateUntilFailureWithResults is a helper tactic which accumulates the list of results obtained from iterating tac until it fails. Always succeeds.

def Lean.Elab.Tactic.iterateUntilFailureCount {m : Type → Type u_1} [Monad m] [MonadExcept Lean.Exception m] {α : Type} (tac : m α) : m Nat

iterateUntilFailureCount is similar to iterateUntilFailure except it counts the number of successful calls to tac. Always succeeds.

Equations

• Lean.Elab.Tactic.iterateUntilFailureCount tac = do let r ← Lean.Elab.Tactic.iterateUntilFailureWithResults tac pure (List.length r)

def Mathlib.getPackageDir (pkg : String) : IO System.FilePath

Returns the root directory which contains the package root file, e.g. Mathlib.lean.

Equations

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

def Mathlib.getMathlibDir : IO System.FilePath

Returns the mathlib root directory.

Equations

• Mathlib.getMathlibDir = Mathlib.getPackageDir "Mathlib"