def
Lean.MVarId.instantiateMVarsInType
{m : Type → Type}
[Monad m]
[Lean.MonadMCtx m]
[Lean.MonadError m]
(mvarId : Lean.MVarId)
:
Instantiate metavariables in the type of the given metavariable, update the metavariable's declaration and return the new type.
Instances For
def
Lean.MVarId.instantiateMVarsInLocalDecl
{m : Type → Type}
[Monad m]
[Lean.MonadMCtx m]
[Lean.MonadError m]
(mvarId : Lean.MVarId)
(fvarId : Lean.FVarId)
:
Instantiate metavariables in the LocalDecl
of the given fvar, update the
LocalDecl
and return the new LocalDecl.
Instances For
def
Lean.MVarId.instantiateMVarsInLocalContext
{m : Type → Type}
[Monad m]
[Lean.MonadMCtx m]
[Lean.MonadError m]
(mvarId : Lean.MVarId)
:
Instantiate metavariables in the local context of the given metavariable, update the metavariable's declaration and return the new local context.
Instances For
def
Lean.MVarId.instantiateMVars
{m : Type → Type}
[Monad m]
[Lean.MonadMCtx m]
[Lean.MonadError m]
(mvarId : Lean.MVarId)
:
m Unit
Instantiate metavariables in the local context and type of the given metavariable.