## Stream: general

### Topic: What are temporary metavariables?

#### Jannis Limperg (May 26 2020 at 16:08):

There are lots of functions for dealing with 'temporary metavariables' in init.meta.type_context. Could anyone explain what these are (as opposed to non-temporary metas)?

#### Simon Hudon (May 26 2020 at 16:19):

I think @Edward Ayers is the best person to answer this

#### Edward Ayers (May 26 2020 at 16:45):

The problem is that metavariables are too slow for some things like matching and rewriting. Because in order to perform a unification you need to carry round a metavariable context and do lots of checks. Temporary metavariables are used in the internals of lean when it needs to unify / match things very quickly. The best description of them is here in the source code.

#### Jannis Limperg (May 26 2020 at 17:19):

Thank you, that comment was very helpful! Unfortunately, based on this, it seems like temporary metas don't work for my application.

Follow-up: If I create a regular meta, can I use it to perform some unification, get the meta assignment (if any) and throw the meta away? Or will Lean be unhappy because the meta remains unassigned?

#### Jannis Limperg (May 26 2020 at 17:29):

Also, based on the comment, it seems like I can't freeze individual metas (i.e. prevent them from being assigned); I can only freeze the entire left-hand side and/or right-hand side of a unification problem. Is that accurate?

#### Gabriel Ebner (May 26 2020 at 17:31):

You could assign local constants to the meta-variables. This also prevents them from being assigned (with something else).

Gabriel is right

#### Edward Ayers (May 26 2020 at 17:32):

but you can now also get the assignment directly with type_context.get_assignment

#### Edward Ayers (May 26 2020 at 17:33):

The idea of type_context was that tactic has a restrictive interface to make it difficult to make a badly formed expression. Whereas the type_context lets you modify the metavariable context and local context directly

#### Jannis Limperg (May 27 2020 at 01:34):

Gabriel Ebner said:

You could assign local constants to the meta-variables. This also prevents them from being assigned (with something else).

Okay, but if I use this to freeze a meta, then I can't unfreeze it any more, right? I guess I could overwrite the assignment with a new meta.

Edward Ayers said:

but you can now also get the assignment directly with type_context.get_assignment

Right. I'll try to use this and some regular metas; let's see if Lean is okay with that.

#### Edward Ayers (May 27 2020 at 11:47):

Once you've assigned a meta to a local, you can't unassign it from tactic. You would have to instantiate the assignment local with a new meta.

#### Jannis Limperg (May 27 2020 at 11:53):

Okay, thanks. Next question (sorry, I'm just finding my way around the API): Is it correct that when unification fails, I can't tell whether this is because the terms cannot be unified or whether the unification strategy is just not powerful enough? I want to distinguish between the unification failures for zero =?= suc x and 2 * x =?= 3 * y.

#### Gabriel Ebner (May 27 2020 at 11:55):

No. As you can probably imagine, non-unifiability is hard to determine.

#### Jannis Limperg (May 27 2020 at 11:59):

Okay, I can see how that would be difficult.

Last updated: May 14 2021 at 07:19 UTC