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
  • One or more equations did not get rendered due to their size.
Instances For

    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

      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

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

        Equations
        Instances For