Documentation

Mathlib.Lean.Meta

Additional utilities in Lean.MVarId #

source
def Lean.MVarId.let (g : Lean.MVarId) (h : Lean.Name) (v : Lean.Expr) (t : optParam (Option Lean.Expr) none) :
Lean.MetaM (Lean.FVarId × Lean.MVarId)

Add the hypothesis h : t, given v : t, and return the new FVarId.

Equations
  • g.let h v t = do let __do_lift ← t.getDM (Lean.Meta.inferType v) let __do_lift ← g.define h __do_lift v __do_lift.intro1P
source
def Lean.MVarId.existsi (mvar : Lean.MVarId) (es : List Lean.Expr) :
Lean.MetaM Lean.MVarId

Has the effect of refine ⟨e₁,e₂,⋯, ?_⟩.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.MVarId.intros! (mvarId : Lean.MVarId) :
Lean.MetaM (Array Lean.FVarId × Lean.MVarId)

Applies intro repeatedly until it fails. We use this instead of Lean.MVarId.intros to allowing unfolding. For example, if we want to do introductions for propositions like ¬p, the ¬ needs to be unfolded into → False, and intros does not do such unfolding.

Equations
source
partial def Lean.MVarId.intros!.run (mvarId : Lean.MVarId) (acc : Array Lean.FVarId) (g : Lean.MVarId) :
Lean.MetaM (Array Lean.FVarId × Lean.MVarId)

Implementation of intros!.

source
def Lean.MVarId.getType'' (mvarId : Lean.MVarId) :
Lean.MetaM Lean.Expr

Get the type the given metavariable after instantiating metavariables and cleaning up annotations.

Equations
  • mvarId.getType'' = do let __do_lift ← mvarId.getType let __do_lift ← Lean.instantiateMVars __do_lift pure __do_lift.cleanupAnnotations
source
def Lean.Elab.Tactic.liftMetaTactic' (tac : Lean.MVarId → Lean.MetaM Lean.MVarId) :
Lean.Elab.Tactic.TacticM Unit

Analogue of liftMetaTactic for tactics that return a single goal.

Equations
source
def Lean.Elab.Tactic.run_for {α : Type} (mvarId : Lean.MVarId) (x : Lean.Elab.Tactic.TacticM α) :
Lean.Elab.TermElabM (Option α × List Lean.MVarId)

Copy of Lean.Elab.Tactic.run that can return a value.

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