Documentation

Lean.Meta.AbstractMVars

@[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.
Instances For

    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.

    If levels := false, then level metavariables are not abstracted.

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