Documentation

Lean.Meta.Tactic.Util

source
def Lean.MVarId.getTag (mvarId : Lean.MVarId) :
Lean.MetaM Lake.Name

Get the user name of the given metavariable.

Instances For
    source
    @[deprecated Lean.MVarId.getTag]
    def Lean.Meta.getMVarTag (mvarId : Lean.MVarId) :
    Lean.MetaM Lake.Name
    Instances For
      source
      def Lean.MVarId.setTag (mvarId : Lean.MVarId) (tag : Lake.Name) :
      Lean.MetaM Unit
      Instances For
        source
        @[deprecated Lean.MVarId.setTag]
        def Lean.Meta.setMVarTag (mvarId : Lean.MVarId) (tag : Lake.Name) :
        Lean.MetaM Unit
        Instances For
          source
          def Lean.Meta.appendTag (tag : Lake.Name) (suffix : Lake.Name) :
          Lake.Name
          Instances For
            source
            def Lean.Meta.appendTagSuffix (mvarId : Lean.MVarId) (suffix : Lake.Name) :
            Lean.MetaM Unit
            Instances For
              source
              def Lean.Meta.mkFreshExprSyntheticOpaqueMVar (type : Lean.Expr) (tag : optParam Lake.Name Lean.Name.anonymous) :
              Lean.MetaM Lean.Expr
              Instances For
                source
                def Lean.Meta.throwTacticEx {α : Type} (tacticName : Lake.Name) (mvarId : Lean.MVarId) (msg : Lean.MessageData) :
                Lean.MetaM α
                Instances For
                  source
                  def Lean.Meta.throwNestedTacticEx {α : Type} (tacticName : Lake.Name) (ex : Lean.Exception) :
                  Lean.MetaM α
                  Instances For
                    source
                    def Lean.MVarId.checkNotAssigned (mvarId : Lean.MVarId) (tacticName : Lake.Name) :
                    Lean.MetaM Unit

                    Throw a tactic exception with given tactic name if the given metavariable is assigned.

                    Instances For
                      source
                      @[deprecated Lean.MVarId.checkNotAssigned]
                      def Lean.Meta.checkNotAssigned (mvarId : Lean.MVarId) (tacticName : Lake.Name) :
                      Lean.MetaM Unit
                      Instances For
                        source
                        def Lean.MVarId.getType (mvarId : Lean.MVarId) :
                        Lean.MetaM Lean.Expr

                        Get the type the given metavariable.

                        Instances For
                          source
                          @[deprecated Lean.MVarId.getType]
                          def Lean.Meta.getMVarType (mvarId : Lean.MVarId) :
                          Lean.MetaM Lean.Expr
                          Instances For
                            source
                            def Lean.MVarId.getType' (mvarId : Lean.MVarId) :
                            Lean.MetaM Lean.Expr

                            Get the type the given metavariable after instantiating metavariables and reducing to weak head normal form.

                            Instances For
                              source
                              @[deprecated Lean.MVarId.getType']
                              def Lean.Meta.getMVarType' (mvarId : Lean.MVarId) :
                              Lean.MetaM Lean.Expr
                              Instances For
                                source
                                def Lean.MVarId.admit (mvarId : Lean.MVarId) (synthetic : optParam Bool true) :
                                Lean.MetaM Unit

                                Assign mvarId to sorryAx

                                Instances For
                                  source
                                  @[deprecated Lean.MVarId.admit]
                                  def Lean.Meta.admit (mvarId : Lean.MVarId) (synthetic : optParam Bool true) :
                                  Lean.MetaM Unit
                                  Instances For
                                    source
                                    def Lean.MVarId.headBetaType (mvarId : Lean.MVarId) :
                                    Lean.MetaM Unit

                                    Beta reduce the metavariable type head

                                    Instances For
                                      source
                                      @[deprecated Lean.MVarId.headBetaType]
                                      def Lean.Meta.headBetaMVarType (mvarId : Lean.MVarId) :
                                      Lean.MetaM Unit
                                      Instances For
                                        source
                                        def Lean.MVarId.getNondepPropHyps (mvarId : Lean.MVarId) :
                                        Lean.MetaM (Array Lean.FVarId)

                                        Collect nondependent hypotheses that are propositions.

                                        Instances For
                                          source
                                          @[deprecated Lean.MVarId.getNondepPropHyps]
                                          def Lean.Meta.getNondepPropHyps (mvarId : Lean.MVarId) :
                                          Lean.MetaM (Array Lean.FVarId)
                                          Instances For
                                            source
                                            def Lean.Meta.saturate (mvarId : Lean.MVarId) (x : Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))) :
                                            Lean.MetaM (List Lean.MVarId)
                                            Instances For
                                              source
                                              partial def Lean.Meta.saturate.go (x : Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))) (mvarId : Lean.MVarId) :
                                              StateRefT' IO.RealWorld (Array Lean.MVarId) Lean.MetaM Unit
                                              source
                                              def Lean.Meta.exactlyOne (mvarIds : List Lean.MVarId) (msg : optParam Lean.MessageData ((Lean.MessageData.ofFormat ∘ Std.format) "unexpected number of goals")) :
                                              Lean.MetaM Lean.MVarId
                                              Instances For
                                                source
                                                def Lean.Meta.ensureAtMostOne (mvarIds : List Lean.MVarId) (msg : optParam Lean.MessageData ((Lean.MessageData.ofFormat ∘ Std.format) "unexpected number of goals")) :
                                                Lean.MetaM (Option Lean.MVarId)
                                                Instances For
                                                  source
                                                  def Lean.Meta.getPropHyps :
                                                  Lean.MetaM (Array Lean.FVarId)

                                                  Return all propositions in the local context.

                                                  Instances For
                                                    source
                                                    def Lean.MVarId.inferInstance (mvarId : Lean.MVarId) :
                                                    Lean.MetaM Unit
                                                    Instances For
                                                      source
                                                      inductive Lean.Meta.TacticResultCNM :
                                                      Type
                                                      Instances For