source
def Lean.MVarId.instantiateMVarsInType {m : Type → Type} [Monad m] [MonadMCtx m] [MonadError m] (mvarId : MVarId) :
m Expr

Instantiate metavariables in the type of the given metavariable, update the metavariable's declaration and return the new type.

Equations

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

Instances For

source
def Lean.MVarId.instantiateMVarsInLocalDecl {m : Type → Type} [Monad m] [MonadMCtx m] [MonadError m] (mvarId : MVarId) (fvarId : FVarId) :
m LocalDecl

Instantiate metavariables in the `LocalDecl` of the given fvar, update the `LocalDecl` and return the new `LocalDecl.`

Equations

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

Instances For

source
def Lean.MVarId.instantiateMVarsInLocalContext {m : Type → Type} [Monad m] [MonadMCtx m] [MonadError m] (mvarId : MVarId) :
m LocalContext

Instantiate metavariables in the local context of the given metavariable, update the metavariable's declaration and return the new local context.

Equations

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

Instances For

source
def Lean.MVarId.instantiateMVars {m : Type → Type} [Monad m] [MonadMCtx m] [MonadError m] (mvarId : MVarId) :
m Unit

Instantiate metavariables in the local context and type of the given metavariable.

Equations

- mvarId.instantiateMVars = do let __do_lift ← Lean.getMCtx discard (__do_lift.getExprMVarDecl mvarId) Lean.instantiateMVarDeclMVars mvarId

Instances For