Documentation

Lean.Meta.AbstractMVars

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

      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