Documentation

Lean.Meta.Tactic.Util

Get the user name of the given metavariable.

Equations
Instances For
    @[deprecated Lean.MVarId.getTag]
    Equations
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[deprecated Lean.MVarId.setTag]
        Equations
        Instances For
          Equations
          Instances For
            Equations
            Instances For
              def Lean.Meta.throwTacticEx {α : Type} (tacticName : Lake.Name) (mvarId : Lean.MVarId) (msg : Lean.MessageData) :
              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

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

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[deprecated Lean.MVarId.checkNotAssigned]
                    Equations
                    Instances For

                      Get the type the given metavariable.

                      Equations
                      Instances For
                        @[deprecated Lean.MVarId.getType]
                        Equations
                        Instances For

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

                          Equations
                          Instances For
                            @[deprecated Lean.MVarId.getType']
                            Equations
                            Instances For

                              Assign mvarId to sorryAx

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                @[deprecated Lean.MVarId.admit]
                                Equations
                                Instances For

                                  Beta reduce the metavariable type head

                                  Equations
                                  Instances For
                                    @[deprecated Lean.MVarId.headBetaType]
                                    Equations
                                    Instances For

                                      Collect nondependent hypotheses that are propositions.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        @[deprecated Lean.MVarId.getNondepPropHyps]
                                        Equations
                                        Instances For
                                          Equations
                                          Instances For
                                            def Lean.Meta.exactlyOne (mvarIds : List Lean.MVarId) (msg : optParam Lean.MessageData ((Lean.MessageData.ofFormat Std.format) "unexpected number of goals")) :
                                            Equations
                                            Instances For
                                              def Lean.Meta.ensureAtMostOne (mvarIds : List Lean.MVarId) (msg : optParam Lean.MessageData ((Lean.MessageData.ofFormat Std.format) "unexpected number of goals")) :
                                              Equations
                                              Instances For

                                                Return all propositions in the local context.

                                                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