# Documentation

Lean.Meta.AbstractMVars

Instances For
Equations
Instances For
@[inline]
Equations
@[always_inline]
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations

Abstract (current depth) metavariables occurring in e. The result contains

• An array of universe level parameters that replaced universe metavariables occurring in e.
• The number of (expr) metavariables abstracted.
• And an expression of the form fun (m_1 : A_1) ... (m_k : A_k) => e', where k equal to the number of (expr) metavariables abstracted, and e' is e after we replace the metavariables.

Example: given f.{?u} ?m1 where ?m1 : ?m2 Nat, ?m2 : Type -> Type. This function returns { levels := #[u], size := 2, expr := (fun (m2 : Type -> Type) (m1 : m2 Nat) => f.{u} m1) }

This API can be used to "transport" to a different metavariable context. Given a new metavariable context, we replace the AbstractMVarsResult.levels with new fresh universe metavariables, and instantiate the (m_i : A_i) in the lambda-expression with new fresh metavariables.

Application: we use this method to cache the results of type class resolution.

Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.