Additions to Lean.Meta.Basic

Likely these already exist somewhere. Pointers welcome.

def Lean.Meta.preservingMCtx {α : Type} (x : MetaM α) : MetaM α

Restore the metavariable context after execution.

def Lean.Meta.forallMetaTelescopeReducingUntilDefEq (e t : Expr) (kind : MetavarKind := MetavarKind.natural) : MetaM (Array Expr × Array BinderInfo × Expr)

This function is similar to forallMetaTelescopeReducing: Given e of the form forall ..xs, A, this combinator will create a new metavariable for each x in xs until it reaches an x whose type is defeq to t, and instantiate A with these, while also reducing A if needed. It uses forallMetaTelescopeReducing.

This function returns a triple (mvs, bis, out) where

• mvs is an array containing the new metavariables.
• bis is an array containing the binder infos for the mvs.
• out is e but instantiated with the mvs.

@[inline]

def Lean.Meta.pureIsDefEq (e₁ e₂ : Expr) : MetaM Bool

pureIsDefEq e₁ e₂ is short for withNewMCtxDepth <| isDefEq e₁ e₂. Determines whether two expressions are definitionally equal to each other when metavariables are not assignable.

def Lean.Meta.mkRel (n : Name) (lhs rhs : Expr) : MetaM Expr

mkRel n lhs rhs is mkAppM n #[lhs, rhs], but with optimizations for Eq and Iff.

def Lean.Meta.withEnsuringLocalInstance {α : Type} (inst : MVarId) (k : MetaM (Expr × α)) : MetaM (Expr × α)

Given a metavariable inst whose type is a class, tries to synthesize the instance then runs k. If synthesis fails, then runs k with inst as a local instance and then substitutes inst into the resulting expression.

Example: reassocExprHom operates by applying simp lemmas that assume a Category instance. The category might not yet be known, which can prevent simp lemmas from applying. We can add inst as a local instance to deal with this. However, if the instance is synthesizable, we prefer running k directly so that the local instance doesn't affect typeclass inference.

def Lean.Meta.ensureHasType (e expectedType : Expr) : MetaM Expr

Checks that e has type expectedType (i.e. that its type is defeq to expectedType at the current transparency). If not, coerces e to this type or fails with a descriptive error.

def Lean.Meta.ensureIsFunction (e : Expr) : MetaM Expr

Checks that e is a function (i.e. that its type is a .forallE after instantiateMVars and whnf). If not, coerces e to a function or fails with a descriptive error.

def Lean.Meta.ensureIsSort (e : Expr) : MetaM Expr

Checks that e is a type (i.e. that its type is a Sort after instantiateMVars and whnf). If not, coerces e to a Sort or fails with a descriptive error.