Documentation

Lean.Elab.Tactic.Basic

Assign mvarId := sorry

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
      • 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
        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
                Equations
                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
                                  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
                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For

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

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