Documentation

Mathlib.Tactic.Core

Generally useful tactics. #

def Lean.toModifiers (nm : Name) (newDoc : Option (TSyntax `Lean.Parser.Command.docComment) := none) :

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

Equations
    Instances For
      def Lean.toPreDefinition (nm newNm : Name) (newType newValue : Expr) (newDoc : Option (TSyntax `Lean.Parser.Command.docComment) := none) :

      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
        Instances For
          def Lean.setProtected {m : TypeType} [MonadEnv m] (nm : Name) :

          Make nm protected.

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

              Introduce variables, giving them names from a specified list.

              Equations
                Instances For

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

                  Equations
                    Instances For

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

                      Equations
                        Instances For

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

                          Equations
                            Instances For

                              Extract the argument from a usingArg syntax as a syntax term

                              Equations
                                Instances For

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

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

                                      Equations
                                        Instances For

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

                                          Equations
                                            Instances For
                                              def Lean.Elab.Tactic.getFVarIdsAt (goal : MVarId) (ids : Option (Array Syntax) := none) (includeImplementationDetails : Bool := false) :

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

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

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

                                                      Equations
                                                        Instances For

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

                                                          Equations
                                                            Instances For
                                                              def Lean.Elab.Tactic.iterateExactly' {m : TypeType u} [Monad m] :
                                                              Natm Unitm Unit

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

                                                              Equations
                                                                Instances For

                                                                  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
                                                                    Instances For
                                                                      partial def Lean.Elab.Tactic.iterateUntilFailure {m : TypeType u} [Monad m] [MonadExcept Exception m] (tac : m Unit) :

                                                                      Repeats a tactic until it fails. Always succeeds.

                                                                      partial def Lean.Elab.Tactic.iterateUntilFailureWithResults {m : TypeType u} [Monad m] [MonadExcept 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 : TypeType u} [Monad m] [MonadExcept 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
                                                                        Instances For

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

                                                                          Equations
                                                                            Instances For

                                                                              Returns the mathlib root directory.

                                                                              Equations
                                                                                Instances For