metavariable details

Stream: general

[Edward Ayers]

In metavar_context.h, the classmetavar_decl keeps a local_context field called m_context, which is the local context in which the mvar was created. In the system description it says "since only closed terms can be assigned to metavariables, a metavariable that occurs in a context records the parameters that it depends on". Is this what m_context is doing? Does closed here mean no unbound de-bruijn variables? The system description seems to imply that the context is stored as a telescope of pis on the type of the mvar rather than in a special field in the declaration which is confusing me. Thanks

[Gabriel Ebner]

The system description describes an old version of Lean where metavariables are handled differently. The metavariables in Lean 3 can have free variables in the form of local constants.

[Gabriel Ebner]

This is also the reason for the delayed_abstraction macro, if you've seen it before. If you want to build λ x, ?m_1 where ?m_1 could contain x as a free variable, then we insert a delayed_abstraction macro that tells Lean to replace the local constant by a de Bruijn variable when instantiating the metavariable.

[Gabriel Ebner]

Re: publications. Many of the publications on the website describe old versions of Lean. I think the ICFP paper from last year (metaprogramming framework for formal verification) and the IJCAR paper from 2016 (congruence closure) are the only two which are up-to-date as of Lean 3.