Documentation

Std.Lean.Meta.InstantiateMVars

source
def Lean.MVarId.instantiateMVarsInType {m : Type → Type} [Monad m] [Lean.MonadMCtx m] [Lean.MonadError m] (mvarId : Lean.MVarId) :
m Lean.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] [Lean.MonadMCtx m] [Lean.MonadError m] (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) :
    m Lean.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] [Lean.MonadMCtx m] [Lean.MonadError m] (mvarId : Lean.MVarId) :
      m Lean.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] [Lean.MonadMCtx m] [Lean.MonadError m] (mvarId : Lean.MVarId) :
        m Unit

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

        Equations
        Instances For