Documentation

Lean.Elab.Tactic.BuiltinTactic

source
def Lean.Elab.Tactic.evalWithAnnotateState :
Tactic
Instances For
    source
    def Lean.Elab.Tactic.evalDone :
    Tactic
    Instances For
      source
      def Lean.Elab.Tactic.evalSepTactics :
      Tactic

      Evaluates a tactic script in form of a syntax node with alternating tactics and separators as children.

      Instances For
        source
        def Lean.Elab.Tactic.evalSeq1 :
        Tactic
        Instances For
          source
          def Lean.Elab.Tactic.evalParen :
          Tactic
          Instances For
            source
            def Lean.Elab.Tactic.evalTacticSeq1Indented :
            Tactic
            Instances For
              source
              def Lean.Elab.Tactic.evalTacticSeqBracketed :
              Tactic
              Instances For
                source
                def Lean.Elab.Tactic.evalTacticCDot :
                Tactic
                Instances For
                  source
                  def Lean.Elab.Tactic.evalFocus :
                  Tactic
                  Instances For
                    source
                    def Lean.Elab.Tactic.evalRotateLeft :
                    Tactic
                    Instances For
                      source
                      def Lean.Elab.Tactic.evalRotateRight :
                      Tactic
                      Instances For
                        source
                        def Lean.Elab.Tactic.evalOpen :
                        Tactic
                        Instances For
                          source
                          def Lean.Elab.Tactic.elabSetOption :
                          Tactic
                          Instances For
                            source
                            def Lean.Elab.Tactic.evalAllGoals :
                            Tactic
                            Instances For
                              source
                              def Lean.Elab.Tactic.evalAnyGoals :
                              Tactic
                              Instances For
                                source
                                def Lean.Elab.Tactic.evalTacticSeq :
                                Tactic
                                Instances For
                                  source
                                  partial def Lean.Elab.Tactic.evalChoiceAux (tactics : Array Syntax) (i : Nat) :
                                  TacticM Unit
                                  source
                                  def Lean.Elab.Tactic.evalChoice :
                                  Tactic
                                  Instances For
                                    source
                                    def Lean.Elab.Tactic.evalSkip :
                                    Tactic
                                    Instances For
                                      source
                                      def Lean.Elab.Tactic.evalUnknown :
                                      Tactic
                                      Instances For
                                        source
                                        def Lean.Elab.Tactic.evalFailIfSuccess :
                                        Tactic
                                        Instances For
                                          source
                                          def Lean.Elab.Tactic.evalTraceState :
                                          Tactic
                                          Instances For
                                            source
                                            def Lean.Elab.Tactic.evalTraceMessage :
                                            Tactic
                                            Instances For
                                              source
                                              def Lean.Elab.Tactic.evalAssumption :
                                              Tactic
                                              Instances For
                                                source
                                                def Lean.Elab.Tactic.evalContradiction :
                                                Tactic
                                                Instances For
                                                  source
                                                  def Lean.Elab.Tactic.evalRefl :
                                                  Tactic
                                                  Instances For
                                                    source
                                                    def Lean.Elab.Tactic.evalIntro :
                                                    Tactic
                                                    Instances For
                                                      source
                                                      def Lean.Elab.Tactic.evalIntroMatch :
                                                      Tactic
                                                      Instances For
                                                        source
                                                        def Lean.Elab.Tactic.evalIntros :
                                                        Tactic
                                                        Instances For
                                                          source
                                                          def Lean.Elab.Tactic.evalRevert :
                                                          Tactic
                                                          Instances For
                                                            source
                                                            def Lean.Elab.Tactic.evalClear :
                                                            Tactic
                                                            Instances For
                                                              source
                                                              def Lean.Elab.Tactic.evalClearValue :
                                                              Tactic
                                                              Instances For
                                                                source
                                                                def Lean.Elab.Tactic.forEachVar (hs : Array Syntax) (tac : MVarId → FVarId → MetaM MVarId) :
                                                                TacticM Unit
                                                                Instances For
                                                                  source
                                                                  def Lean.Elab.Tactic.evalSubst :
                                                                  Tactic
                                                                  Instances For
                                                                    source
                                                                    def Lean.Elab.Tactic.evalSubstVars :
                                                                    Tactic
                                                                    Instances For
                                                                      source
                                                                      def Lean.Elab.Tactic.evalSubstEqs :
                                                                      Tactic
                                                                      Instances For
                                                                        source
                                                                        def Lean.Elab.Tactic.evalCase :
                                                                        Tactic
                                                                        Instances For
                                                                          source
                                                                          def Lean.Elab.Tactic.evalCase' :
                                                                          Tactic
                                                                          Instances For
                                                                            source
                                                                            def Lean.Elab.Tactic.evalRenameInaccessibles :
                                                                            Tactic
                                                                            Instances For
                                                                              source
                                                                              def Lean.Elab.Tactic.evalFirst :
                                                                              Tactic
                                                                              Instances For
                                                                                source
                                                                                def Lean.Elab.Tactic.evalFail :
                                                                                Tactic
                                                                                Instances For
                                                                                  source
                                                                                  def Lean.Elab.Tactic.evalDbgTrace :
                                                                                  Tactic
                                                                                  Instances For
                                                                                    source
                                                                                    def Lean.Elab.Tactic.evalSleep :
                                                                                    Tactic
                                                                                    Instances For
                                                                                      source
                                                                                      def Lean.Elab.Tactic.evalLeft :
                                                                                      Tactic
                                                                                      Instances For
                                                                                        source
                                                                                        def Lean.Elab.Tactic.evalRight :
                                                                                        Tactic
                                                                                        Instances For
                                                                                          source
                                                                                          def Lean.Elab.Tactic.evalReplace :
                                                                                          Tactic
                                                                                          Instances For
                                                                                            source
                                                                                            def Lean.Elab.Tactic.evalRunTac :
                                                                                            Tactic
                                                                                            Instances For