Documentation

Lean.Meta.Tactic.Util

Get the user name of the given metavariable.

Equations
    Instances For
      def Lean.MVarId.setTag (mvarId : MVarId) (tag : Name) :
      Equations
        Instances For
          def Lean.Meta.appendTag (tag suffix : Name) :
          Equations
            Instances For
              def Lean.Meta.appendTagSuffix (mvarId : MVarId) (suffix : Name) :
              Equations
                Instances For
                  Equations
                    Instances For
                      def Lean.Meta.throwTacticEx {α : Type} (tacticName : Name) (mvarId : MVarId) (msg? : Option MessageData := none) :
                      Equations
                        Instances For
                          def Lean.Meta.throwNestedTacticEx {α : Type} (tacticName : Name) (ex : Exception) :
                          Equations
                            Instances For
                              def Lean.MVarId.checkNotAssigned (mvarId : MVarId) (tacticName : Name) :

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

                              Equations
                                Instances For

                                  Get the type the given metavariable.

                                  Equations
                                    Instances For

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

                                      Equations
                                        Instances For
                                          def Lean.MVarId.admit (mvarId : MVarId) (synthetic : Bool := true) :

                                          Assign mvarId to sorryAx

                                          Equations
                                            Instances For

                                              Beta reduce the metavariable type head

                                              Equations
                                                Instances For

                                                  Collect nondependent hypotheses that are propositions.

                                                  Equations
                                                    Instances For
                                                      Equations
                                                        Instances For
                                                          def Lean.Meta.exactlyOne (mvarIds : List MVarId) (msg : MessageData := (MessageData.ofFormat format) "unexpected number of goals") :
                                                          Equations
                                                            Instances For
                                                              def Lean.Meta.ensureAtMostOne (mvarIds : List MVarId) (msg : MessageData := (MessageData.ofFormat format) "unexpected number of goals") :
                                                              Equations
                                                                Instances For

                                                                  Return all propositions in the local context.

                                                                  Equations
                                                                    Instances For
                                                                      Equations
                                                                        Instances For
                                                                          Instances For

                                                                            Check if a goal is of a subsingleton type.

                                                                            Equations
                                                                              Instances For