Additional utilities in Lean.MVarId

def Lean.MVarId.synthInstance (g : Lean.MVarId) : Lean.MetaM Unit

Solve a goal by synthesizing an instance.

Equations

• Lean.MVarId.synthInstance g = do let __do_lift ← Lean.MVarId.getType g let __do_lift ← Lean.Meta.synthInstance __do_lift none Lean.MVarId.assign g __do_lift

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

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

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

def Lean.MVarId.applyConst (mvar : Lean.MVarId) (c : Lean.Name) (cfg : optParam Lean.Meta.ApplyConfig { newGoals := Lean.Meta.ApplyNewGoals.nonDependentFirst, synthAssignedInstances := true, allowSynthFailures := false, approx := true }) : Lean.MetaM (List Lean.MVarId)

Short-hand for applying a constant to the goal.

Equations

• Lean.MVarId.applyConst mvar c cfg = do let __do_lift ← Lean.Meta.mkConstWithFreshMVarLevels c Lean.MVarId.apply mvar __do_lift cfg

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.

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

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

def Lean.MVarId.subsingleton? (g : Lean.MVarId) : Lean.MetaM Bool

Check if a goal is of a subsingleton type.

Equations

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

def Lean.MVarId.independent? (L : List Lean.MVarId) (g : Lean.MVarId) : Lean.MetaM Bool

Check if a goal is "independent" of a list of other goals. We say a goal is independent of other goals if assigning a value to it can not change the solvability of the other goals.

This function only calculates a conservative approximation of this condition.

Equations

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

def Lean.MVarId.iffOfEq (mvarId : Lean.MVarId) : Lean.MetaM Lean.MVarId

Try to convert an Iff into an Eq by applying iff_of_eq. If successful, returns the new goal, and otherwise returns the original MVarId.

This may be regarded as being a special case of Lean.MVarId.liftReflToEq, specifically for Iff.

Equations

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

def Lean.MVarId.propext (mvarId : Lean.MVarId) : Lean.MetaM Lean.MVarId

Try to convert an Eq into an Iff by applying propext. If successful, then returns then new goal, otherwise returns the original MVarId.

Equations

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

def Lean.MVarId.proofIrrelHeq (mvarId : Lean.MVarId) : Lean.MetaM Bool

Try to close the goal with using proof_irrel_heq. Returns whether or not it succeeds.

We need to be somewhat careful not to assign metavariables while doing this, otherwise we might specialize Sort _ to Prop.

Equations

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

def Lean.MVarId.subsingletonElim (mvarId : Lean.MVarId) : Lean.MetaM Bool

Try to close the goal using Subsingleton.elim. Returns whether or not it succeeds.

We are careful to apply Subsingleton.elim in a way that does not assign any metavariables. This is to prevent the Subsingleton Prop instance from being used as justification to specialize Sort _ to Prop.

Equations

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

def Lean.Meta.getLocalHyps {m : Type → Type} [Monad m] [Lean.MonadLCtx m] : m (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.

def Lean.Meta.countLocalHypsUsed {m : Type → Type} [Monad m] [Lean.MonadLCtx m] [Lean.MonadMCtx m] (e : Lean.Expr) : m Nat

Count how many local hypotheses appear in an expression.

Equations

• Lean.Meta.countLocalHypsUsed e = do let e' ← Lean.instantiateMVars e let __do_lift ← Lean.Meta.getLocalHyps pure (List.countP (fun h => Lean.Expr.occurs h e') (Array.toList __do_lift))

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.

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

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

• Lean.MVarId.getType'' mvarId = do let __do_lift ← Lean.MVarId.getType mvarId let __do_lift ← Lean.instantiateMVars __do_lift pure (Lean.Expr.cleanupAnnotations __do_lift)

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]

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.