Zulip Chat Archive

Stream: general

Topic: What are temporary metavariables?


view this post on Zulip 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)?

view this post on Zulip Simon Hudon (May 26 2020 at 16:19):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip Edward Ayers (May 26 2020 at 17:31):

Gabriel is right

view this post on Zulip Edward Ayers (May 26 2020 at 17:32):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Gabriel Ebner (May 27 2020 at 11:55):

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

view this post on Zulip 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