Documentation

Lean.Meta.Tactic.Intro

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    def Lean.Meta.introNCore (mvarId : Lean.MVarId) (n : Nat) (givenNames : List Lake.Name) (useNamesForExplicitOnly : Bool) (preserveBinderNames : Bool) :
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[inline, reducible]
      abbrev Lean.MVarId.introN (mvarId : Lean.MVarId) (n : Nat) (givenNames : optParam (List Lake.Name) []) (useNamesForExplicitOnly : optParam Bool false) :

      Introduce n binders in the goal mvarId.

      Equations
      Instances For
        @[inline, reducible, deprecated Lean.MVarId.introN]
        abbrev Lean.Meta.introN (mvarId : Lean.MVarId) (n : Nat) (givenNames : optParam (List Lake.Name) []) (useNamesForExplicitOnly : optParam Bool false) :
        Equations
        Instances For
          @[inline, reducible]

          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
            @[inline, reducible, deprecated Lean.MVarId.introNP]
            Equations
            Instances For

              Introduce one binder using name as the the new hypothesis name.

              Equations
              Instances For
                @[deprecated Lean.MVarId.intro]
                Equations
                Instances For
                  def Lean.Meta.intro1Core (mvarId : Lean.MVarId) (preserveBinderNames : Bool) :
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[inline, reducible]

                    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
                      @[inline, reducible, deprecated Lean.MVarId.intro1]
                      Equations
                      Instances For
                        @[inline, reducible]

                        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
                          @[inline, reducible, deprecated Lean.MVarId.intro1P]
                          Equations
                          Instances For

                            Introduce as many binders as possible without unfolding definitions.

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