def Lean.Elab.Tactic.Do.ProofMode.mIntro {m : Type → Type u_1} {α : Type} [Monad m] [MonadControlT MetaM m] (goal : MGoal) (ident : TSyntax `Lean.binderIdent) (k : MGoal → m (α × Expr)) : m (α × Expr)

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Tactic.Do.ProofMode.mIntroForall {m : Type → Type u_1} {α : Type} [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m] (goal : MGoal) (ident : TSyntax `Lean.binderIdent) (k : MGoal → m (α × Expr)) : m (α × Expr)

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Tactic.Do.ProofMode.mIntroForallN {m : Type → Type u_1} {α : Type} [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m] (goal : MGoal) (n : Nat) (k : MGoal → m (α × Expr)) : m (α × Expr)

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Tactic.Do.ProofMode.mIntroForallN goal 0 k = k goal

def Lean.Elab.Tactic.Do.ProofMode.elabMIntro : Tactic

Equations

• One or more equations did not get rendered due to their size.