# Additions to `Lean.Meta.Basic`

#

Likely these already exist somewhere. Pointers welcome.

Restore the metavariable context after execution.

## Equations

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

## Instances For

def
Lean.Meta.forallMetaTelescopeReducingUntilDefEq
(e : Lean.Expr)
(t : Lean.Expr)
(kind : optParam Lean.MetavarKind Lean.MetavarKind.natural)
:

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.

## Instances For

@[inline]

`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₂)