Documentation

Lean.Meta.Tactic.Intro

Similar to Lean.Core.mkFreshUserName, but takes into account the tactic.hygienic option value. If tactic.hygienic = true, then fresh macro scopes are applied to binderName. If not, then returns an (accessible) name based on binderName that is unused in the local context.

Equations
    Instances For
      def Lean.Meta.introNCore (mvarId : MVarId) (n : Nat) (givenNames : List Name) (useNamesForExplicitOnly preserveBinderNames : Bool) :
      Equations
        Instances For
          @[reducible, inline]
          abbrev Lean.MVarId.introN (mvarId : MVarId) (n : Nat) (givenNames : List Name := []) (useNamesForExplicitOnly : Bool := false) :

          Introduce n binders in the goal mvarId.

          Equations
            Instances For
              @[reducible, inline]

              Introduce n binders in the goal mvarId. The new hypotheses are named using the binder names. The suffix P stands for "preserving`.

              Equations
                Instances For
                  def Lean.MVarId.intro (mvarId : MVarId) (name : Name) :

                  Introduce one binder using name as the new hypothesis name.

                  Equations
                    Instances For
                      def Lean.Meta.intro1Core (mvarId : MVarId) (preserveBinderNames : Bool) :
                      Equations
                        Instances For
                          @[reducible, inline]

                          Introduce one object from the goal mvarid, without preserving the name used in the binder. Returns a pair made of the newly introduced variable (which will have an inaccessible name) and the new goal. This will fail if there is nothing to introduce, ie when the goal does not start with a forall, lambda or let.

                          Equations
                            Instances For
                              @[reducible, inline]

                              Introduce one object from the goal mvarid, preserving the name used in the binder. Returns a pair made of the newly introduced variable and the new goal. This will fail if there is nothing to introduce, ie when the goal does not start with a forall, lambda or let.

                              Equations
                                Instances For

                                  Calculate the number of new hypotheses that would be created by intros, i.e. the number of binders which can be introduced without unfolding definitions.

                                  Introduce as many binders as possible without unfolding definitions.

                                  Equations
                                    Instances For