Additional utilities in Lean.MVarId

ink

def Lean.MVarId.replace (g : Lean.MVarId) (hyp : Lean.FVarId) (proof : Lean.Expr) (typeNew : optParam (Option Lean.Expr) none) : Lean.MetaM Lean.Meta.AssertAfterResult

Replace hypothesis hyp in goal g with proof : typeNew. The new hypothesis is given the same user name as the original, it attempts to avoid reordering hypotheses, and the original is cleared if possible.

Equations

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

ink

def Lean.MVarId.replace.findMaxFVar (e : Lean.Expr) : StateRefT' IO.RealWorld Lean.LocalDecl Lean.MetaM Unit

Finds the LocalDecl for the FVar in e with the highest index.

Equations

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

ink

def Lean.MVarId.note (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

• Lean.MVarId.note g h v t = do let __do_lift ← Option.getDM t (Lean.Meta.inferType v) let __do_lift ← Lean.MVarId.assert g h __do_lift v Lean.MVarId.intro1P __do_lift

ink

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.

ink

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

• Lean.MVarId.intros! mvarId = Lean.MVarId.intros!.run mvarId #[] mvarId

ink

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!.

ink

def Lean.Meta.getLocalHyps : Lean.MetaM (Array Lean.Expr)

Return local hypotheses which are not "implementation detail", as Exprs.

Equations

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

ink

def Lean.Meta.mapForallTelescope' (F : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr) (forallTerm : Lean.Expr) : Lean.MetaM Lean.Expr

Given a monadic function F that takes a type and a term of that type and produces a new term, lifts this to the monadic function that opens a ∀ telescope, applies F to the body, and then builds the lambda telescope term for the new term.

Equations

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

ink

def Lean.Meta.mapForallTelescope (F : Lean.Expr → Lean.MetaM Lean.Expr) (forallTerm : Lean.Expr) : Lean.MetaM Lean.Expr

Given a monadic function F that takes a term and produces a new term, lifts this to the monadic function that opens a ∀ telescope, applies F to the body, and then builds the lambda telescope term for the new term.

Equations

• Lean.Meta.mapForallTelescope F forallTerm = Lean.Meta.mapForallTelescope' (fun x e => F e) forallTerm

ink

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

• Lean.Elab.Tactic.liftMetaTactic' tac = Lean.Elab.Tactic.liftMetaTactic fun g => do let __do_lift ← tac g pure [__do_lift]

ink

def Lean.Elab.Tactic.liftMetaFinishingTactic (tac : Lean.MVarId → Lean.MetaM Unit) : Lean.Elab.Tactic.TacticM Unit

Analogue of liftMetaTactic for tactics that do not return any goals.

Equations

• Lean.Elab.Tactic.liftMetaFinishingTactic tac = Lean.Elab.Tactic.liftMetaTactic fun g => do tac g pure []

ink

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.