Helper Meta-related functions.
def
Lean.Meta.withLambdaBody
{α : Type}
(e : Lean.Expr)
(x : Lean.Expr → Lean.Expr → Lean.MetaM α)
:
Open lambda-expression by introducing a new local declaration. Similar to lambdaTelescope, but
for only one variable.
Equations
- One or more equations did not get rendered due to their size.
def
Lean.Meta.withLocalDeclsDNondep
{m : Type → Type u_1}
[MonadControlT Lean.MetaM m]
[Monad m]
{α : Type}
[Inhabited α]
(declInfos : Array (Lean.Name × Lean.Expr))
(k : Array Lean.Expr → m α)
:
m α
Add local declarations where the type constructor is trivial (non-dependant on the other declarations).
Equations
- One or more equations did not get rendered due to their size.
def
Lean.Meta.withLetDecls
{m : Type → Type u_1}
[MonadControlT Lean.MetaM m]
[Monad m]
{α : Type}
[Inhabited α]
(declInfos : Array (Lean.Name × (Array Lean.Expr → m Lean.Expr) × (Array Lean.Expr → m Lean.Expr)))
(k : Array Lean.Expr → m α)
:
m α
Introduce let declarations into the local context.
Equations
- Lean.Meta.withLetDecls declInfos k = Lean.Meta.withLetDecls.loop declInfos k #[]
def
Lean.Meta.runTactic
(goal : Lean.MVarId)
(tac : Lean.MVarId → Lean.Elab.Tactic.TacticM (List Lean.MVarId))
:
Run a tactic on a goal in MetaM.
Equations
- One or more equations did not get rendered due to their size.