Documentation

Lean.Elab.Tactic.Do.ProofMode.Intro

source
def Lean.Elab.Tactic.Do.ProofMode.mIntro {m : Type → Type u_1} [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m] (goal : MGoal) (ident : TSyntax `Lean.binderIdent) (k : MGoal → m Expr) :
m Expr
Equations
    Instances For
      source
      def Lean.Elab.Tactic.Do.ProofMode.mIntroForall {m : Type → Type u_1} [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m] (goal : MGoal) (ident : TSyntax `Lean.binderIdent) (k : MGoal → m Expr) :
      m Expr
      Equations
        Instances For
          source
          def Lean.Elab.Tactic.Do.ProofMode.mIntroForallN {m : Type → Type u_1} [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m] (goal : MGoal) (n : Nat) (k : MGoal → m Expr) :
          m Expr
          Equations
            Instances For
              source
              def Lean.Elab.Tactic.Do.ProofMode.elabMIntro :
              Tactic
              Equations
                Instances For