Additions to Lean.Meta.Basic

Likely these already exist somewhere. Pointers welcome.

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

Restore the metavariable context after execution.

Equations

• Lean.Meta.preservingMCtx x = do let mctx ← Lean.getMCtx tryFinally x (Lean.setMCtx mctx)

def Lean.Meta.forallMetaTelescopeReducingUntilDefEq (e t : Lean.Expr) (kind : Lean.MetavarKind := Lean.MetavarKind.natural) : Lean.MetaM (Array Lean.Expr × Array Lean.BinderInfo × Lean.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.

Equations

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

@[inline]

def Lean.Meta.pureIsDefEq (e₁ e₂ : Lean.Expr) : Lean.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.

Equations

• Lean.Meta.pureIsDefEq e₁ e₂ = Lean.Meta.withNewMCtxDepth (Lean.Meta.isDefEq e₁ e₂)

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

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

Equations

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