Documentation

Std.Lean.Meta.InstantiateMVars

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

Instances For

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

    Instances For

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

      Instances For

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

        Instances For