Documentation
Lean
.
Elab
.
Tactic
.
Do
.
ProofMode
.
Intro
Search
return to top
source
Imports
Std.Tactic.Do.Syntax
Lean.Elab.Tactic.Do.ProofMode.Basic
Imported by
Lean
.
Elab
.
Tactic
.
Do
.
ProofMode
.
mIntro
Lean
.
Elab
.
Tactic
.
Do
.
ProofMode
.
mIntroForall
Lean
.
Elab
.
Tactic
.
Do
.
ProofMode
.
mIntroForallN
Lean
.
Elab
.
Tactic
.
Do
.
ProofMode
.
elabMIntro
source
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
Instances For
source
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
Instances For
source
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
Instances For
source
def
Lean
.
Elab
.
Tactic
.
Do
.
ProofMode
.
elabMIntro
:
Tactic
Equations
Instances For