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
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 themvs
.out
ise
but instantiated with themvs
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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₂)
Instances For
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.
Equations
- One or more equations did not get rendered due to their size.