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
        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 #[]]

                  Incremental reuse primitive: if reusableResult? is none, runs act and returns its result together with the saved monadic state after act including the heartbeats used by it. If reusableResult? on the other hand is some (a, state), restores full state including heartbeats used and returns (a, state).

                  The intention is for steps that support incremental reuse to initially pass none as reusableResult? and store the result and state in a snapshot. In a further run, if reuse is possible, reusableResult? should be set to the previous result and state, ensuring that the state after running withRestoreOrSaveFull is identical in both runs. Note however that necessarily this is only an approximation in the case of heartbeats as heartbeats used by withRestoreOrSaveFull itself after calling act as well as by reuse-handling code such as the one supplying reusableResult? are not accounted 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

                          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

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