Documentation

Lean.Elab.Tactic.Basic

Assign mvarId := sorry

Equations
Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      • elaborator : Lake.Name

        Declaration name of the executing elaborator, used by mkTacticInfo to persist it in the info tree

      • recover : Bool

        If true, enable "error recovery" in some tactics. For example, cases tactic admits unsolved alternatives when recover == true. The combinator withoutRecover <tac> disables "error recovery" while executing <tac>. This is useful for tactics such as first | ... | ....

      Instances For
        Equations
        Equations
        Instances For
          Equations
          Instances For
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              Equations
              Instances For
                Equations
                • b.restore restoreInfo = do liftM (b.term.restore restoreInfo) set b.tactic
                Instances For
                  @[specialize #[]]

                  Like Meta.withRestoreOrSaveFull for TermElabM, but also takes a tacSnap? that

                  • when running act, is set as Context.tacSnap?
                  • otherwise (i.e. on restore) is used to update the new snapshot promise to the old task's value. This extra restore step is necessary because while reusableResult? can be used to replay any effects on State, Context.tacSnap? is not part of it but changed via an IO side effect, so it needs to be replayed separately.

                  We use an explicit parameter instead of accessing Context.tacSnap? directly because this prevents withRestoreOrSaveFull and withReader from being used in the wrong order.

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

                        Important: we must define evalTactic before we define the instance MonadExcept for TacticM since it backtracks the state including error messages, and this is bad when rethrowing the exception at the catch block in these methods. We marked these places with a (*) in these methods.

                        Auxiliary datastructure for capturing exceptions at evalTactic.

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

                                  Close the main goal using the given tactic. If it fails, log the error and admit

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    @[inline]
                                    Equations
                                    Instances For
                                      Equations

                                      Execute x with error recovery disabled

                                      Equations
                                      Instances For
                                        Equations
                                        • Lean.Elab.Tactic.instOrElseTacticM = { orElse := Lean.Elab.Tactic.orElse }

                                        Save the current tactic state for a token stx. This method is a no-op if stx has no position information. We use this method to save the tactic state at punctuation such as ;

                                        Equations
                                        Instances For
                                          @[inline]

                                          Elaborate x with stx on the macro stack

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

                                            Adapt a syntax transformation to a regular tactic evaluator.

                                            Equations
                                            Instances For

                                              Add the given goals at the end of the current goals collection.

                                              Equations
                                              Instances For

                                                Discard the first goal and replace it by the given list of goals, keeping the other goals.

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

                                                    Return the main goal metavariable declaration.

                                                    Equations
                                                    Instances For

                                                      Return the main goal tag.

                                                      Equations
                                                      Instances For

                                                        Return expected type for the main goal.

                                                        Equations
                                                        Instances For

                                                          Execute x using the main goal local context and instances

                                                          Equations
                                                          Instances For

                                                            Evaluate tac at mvarId, and return the list of resulting subgoals.

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

                                                              Like evalTacticAt, but without restoring the goal list or pruning solved goals. Useful when these tasks are already being done in an outer loop.

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

                                                                  Closes main goal using the given expression. If checkUnassigned == true, then val must not contain unassigned metavariables. Returns true if val was successfully used to close the goal.

                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For
                                                                    @[inline]
                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For
                                                                      @[inline]

                                                                      Get the mvarid of the main goal, run the given tactic, then set the new goals to be the resulting goal list.

                                                                      Equations
                                                                      Instances For
                                                                        @[inline]
                                                                        Equations
                                                                        • One or more equations did not get rendered due to their size.
                                                                        Instances For
                                                                          @[inline]

                                                                          Analogue of liftMetaTactic for tactics that do not return any goals.

                                                                          Equations
                                                                          Instances For
                                                                            Equations
                                                                            Instances For

                                                                              Use parentTag to tag untagged goals at newGoals. If there are multiple new untagged goals, they are named using <parentTag>.<newSuffix>_<idx> where idx > 0. If there is only one new untagged goal, then we just use parentTag

                                                                              Equations
                                                                              • One or more equations did not get rendered due to their size.
                                                                              Instances For
                                                                                Equations
                                                                                Instances For
                                                                                  def Lean.Elab.Tactic.withCaseRef {m : TypeType} {α : Type} [Monad m] [Lean.MonadRef m] (arrow : Lean.Syntax) (body : Lean.Syntax) (x : m α) :
                                                                                  m α

                                                                                  Use position of => $body for error messages. If there is a line break before body, the message will be displayed on => only, but the "full range" for the info view will still include body.

                                                                                  Equations
                                                                                  Instances For