appendMCtx or mergeMCtx

Stream: lean4

[Tomas Skrivan]

Is there a function that takes to local contexts and merges them together?

Probably #XY problem, I have a mctx : MetavarContext and I want to add it to the current context. The only function that I found is withMCtx that completely replaces the current metavariable context.

Even more #XY, I have two expressions x y : Exprliving in two different metavariable contexts and I want to know if they are defeq. I want to merge those contexts and call isDefEq x y.

[Wojciech Nawrocki]

@Tomas Skrivan what if x is ?m_1 coming from mvar context A and y is ?n_1 coming from mvar context B? In general, the question of defeq doesn't seem to make sense unless both terms live in the same context.

[Tomas Skrivan]

Asking it in the union of A and B should make sense, no?

[Tomas Skrivan]

Of course, the union of A and B does not have to be always well formed. (or well typed, I do not know the exact terminology used here)

[Gabriel Ebner]

The general answer is: you don't. Another thing that could go wrong, which you didn't mention yet, is that the two metavariable contexts might have different assignments for the metavariables.

[Gabriel Ebner]

What do you actually want to do?

[Gabriel Ebner]

Sometimes, a reasonable substitute is to turn a term like f ?m_1 ?m_2 into a lambda-abstraction like fun x y => f x y to transport it to the other metavariable context (and then create new metavariables there and instantiate the lambda-abstraction).

[Tomas Skrivan]

I'm parsing a term from a custom parametric attribute, see simp guard thread.

In the case of @[simp_guard g (λ x => x)] the term I get from the elaborator is (λ x : ?m => x). At some point I want to test if another expression is equal to (λ x : ?m => x), so I need to somehow carry around the created metavariable and use it correctly.

[Tomas Skrivan]

As you suggested, turning those metavariables to bound variables and then assigning fresh metavariables at the equality check would work.

[Tomas Skrivan]

Gabriel Ebner said:

turn a term like f ?m_1 ?m_2 into a lambda-abstraction like fun x y => f x y t

What is the easy/clean way of doing this?