Documentation

Lean.Elab.Tactic.Basic

Assign mvarId := sorry

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 disables "error recovery" while executing . This is useful for tactics such as first | ... | ....

    Instances For
      @[inline, reducible]
      Instances For
        @[inline, reducible]
        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

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

            Instances For

              Execute x with error recovery disabled

              Instances For

                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 ;

                Instances For
                  @[inline]

                  Elaborate x with stx on the macro stack

                  Instances For

                    Adapt a syntax transformation to a regular tactic evaluator.

                    Instances For

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

                      Instances For

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

                        Instances For
                          Equations
                          Instances For

                            Return the main goal metavariable declaration.

                            Instances For

                              Return the main goal tag.

                              Instances For

                                Return expected type for the main goal.

                                Instances For

                                  Execute x using the main goal local context and instances

                                  Instances For

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

                                    Instances For

                                      Close main goal using the given expression. If checkUnassigned == true, then val must not contain unassigned metavariables.

                                      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.

                                        Instances For

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

                                          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.

                                            Instances For