Documentation

Batteries.Lean.Meta.InstantiateMVars

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

Equations
    Instances For

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

      Equations
        Instances For

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

          Equations
            Instances For
              def Lean.MVarId.instantiateMVars {m : TypeType} [Monad m] [MonadMCtx m] [MonadError m] (mvarId : MVarId) :

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

              Equations
                Instances For